Documentation Verification Report

MultipleTransitivity

📁 Source: Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

Statistics

Metric	Count
Definitions `IsMultiplyPretransitive`, `embMap`, `zeroEmbeddingMap`, `addActionHom_embedding`, `mulActionHom_embedding`, `IsMultiplyPretransitive`, `embMap`, `oneEmbeddingMap`	8
Theorems `of_embedding`, `of_embedding_congr`, `isMultiplyPretransitive_iff`, `isMultiplyPretransitive_of_le`, `isMultiplyPretransitive_of_le'`, `isPreprimitive_of_is_two_pretransitive`, `isPretransitive_of_is_two_pretransitive`, `is_two_pretransitive_iff`, `is_zero_pretransitive`, `is_zero_pretransitive'`, `is_zero_pretransitive_iff`, `zeroEmbedding_isPretransitive_iff`, `zeroEmbeddingMap_bijective`, `isMultiplyPretransitive`, `isPreprimitive_of_three_le_card`, `isPretransitive_of_three_le_card`, `isTrivialBlock_of_isBlock`, `eq_top_if_isMultiplyPretransitive`, `eq_top_of_isMultiplyPretransitive`, `instIsPreprimitive`, `isMultiplyPretransitive`, `addActionHom_embedding_isBijective`, `mulActionHom_embedding_isBijective`, `addActionHom_embedding_apply`, `addActionHom_embedding_isInjective`, `mulActionHom_embedding_apply`, `mulActionHom_embedding_isInjective`, `alternatingGroup_le`, `index_of_fixingSubgroup_eq`, `index_of_fixingSubgroup_mul`, `of_embedding`, `of_embedding_congr`, `isMultiplyPretransitive_iff`, `isMultiplyPretransitive_of_le`, `isMultiplyPretransitive_of_le'`, `isPreprimitive_of_is_two_pretransitive`, `isPretransitive_of_is_two_pretransitive`, `is_one_pretransitive_iff`, `is_two_pretransitive_iff`, `is_zero_pretransitive`, `is_zero_pretransitive'`, `oneEmbedding_isPretransitive_iff`, `oneEmbeddingMap_bijective`, `isMultiplyPretransitive`, `isMultiplyPretransitive'`, `isMultiplyPretransitive`, `isMultiplyPretransitive_iff`, `isMultiplyPretransitive_iff_of_conj`, `isPretransitive_iff`, `isPretransitive_iff_of_conj`, `isMultiplyPretransitive`, `isMultiplyPretransitive'`, `isMultiplyPretransitive`, `isMultiplyPretransitive_iff`, `isMultiplyPretransitive_iff_of_conj`, `isPretransitive_iff`, `isPretransitive_iff_of_conj`, `isMultiplyPretransitive`, `isPreprimitive_of_three_le_card`, `isPretransitive_of_three_le_card`, `isTrivialBlock_of_isBlock`	61
Total	69

AddAction

Definitions

Name	Category	Theorems
`IsMultiplyPretransitive` 📖	MathDef	14 math math: `is_zero_pretransitive'`, `SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `isMultiplyPretransitive_of_le`, `SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive`, `SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive'`, `IsMultiplyPreprimitive.isMultiplyPretransitive`, `isMultiplyPretransitive_of_le'`, `instIsMultiplyPretransitiveOfIsMultiplyPreprimitive`, `SubAddAction.ofStabilizer.isMultiplyPretransitive_iff`, `is_two_pretransitive_iff`, `isMultiplyPreprimitive_iff`, `isMultiplyPretransitive_iff`, `SubAddAction.ofStabilizer.isMultiplyPretransitive`, `is_zero_pretransitive_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `HVAdd.hVAdd` `Function.Embedding` `instHVAdd` `Function.Embedding.vadd`	—	`isPretransitive_iff`
`isMultiplyPretransitive_of_le` 📖	mathematical	`Nat.card`	`IsMultiplyPretransitive`	—	`IsPretransitive.of_surjective_map` `Fin.Embedding.restrictSurjective_of_add_le_natCard`
`isMultiplyPretransitive_of_le'` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`IsMultiplyPretransitive`	—	`IsPretransitive.of_surjective_map` `Fin.Embedding.restrictSurjective_of_add_le_ENatCard`
`isPreprimitive_of_is_two_pretransitive` 📖	mathematical	—	`IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`isPretransitive_of_is_two_pretransitive` `Set.subsingleton_or_nontrivial` `Set.top_eq_univ` `eq_top_iff` `is_two_pretransitive_iff` `isBlock_iff_vadd_eq_of_mem` `Set.vadd_mem_vadd_set`
`isPretransitive_of_is_two_pretransitive` 📖	mathematical	—	`IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`zero_vadd` `is_two_pretransitive_iff`
`is_two_pretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`exists_vadd_eq` `Function.Embedding.embFinTwo_apply_zero` `Function.Embedding.vadd_apply` `Function.Embedding.embFinTwo_apply_one` `Function.Embedding.injective` `Function.Embedding.ext` `Fin.eq_one_of_ne_zero`
`is_zero_pretransitive` 📖	mathematical	—	`IsPretransitive` `Function.Embedding` `Function.Embedding.vadd`	—	`instIsPretransitiveOfSubsingleton` `Unique.instSubsingleton`
`is_zero_pretransitive'` 📖	mathematical	—	`IsMultiplyPretransitive`	—	`instIsPretransitiveOfSubsingleton` `Unique.instSubsingleton` `Fin.isEmpty'`
`is_zero_pretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`zeroEmbedding_isPretransitive_iff`
`zeroEmbedding_isPretransitive_iff` 📖	mathematical	—	`IsPretransitive` `Function.Embedding` `Function.Embedding.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`isPretransitive_congr` `AddActionHom.zeroEmbeddingMap_bijective`

AddAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_embedding` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`AddAction.IsPretransitive` `Function.Embedding` `Function.Embedding.vadd`	—	`Function.surjInv_eq` `exists_vadd_eq` `Function.Embedding.ext` `Function.Embedding.vadd_apply` `DFunLike.ext_iff` `AddActionHom.map_vadd'`
`of_embedding_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`AddAction.IsPretransitive` `Function.Embedding` `Function.Embedding.vadd`	—	`AddAction.isPretransitive_congr` `Function.Bijective.injective` `Function.Bijective.addActionHom_embedding_isBijective`

AddActionHom

Definitions

Name	Category	Theorems
`embMap` 📖	CompOp	—
`zeroEmbeddingMap` 📖	CompOp	1 math math: `zeroEmbeddingMap_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`zeroEmbeddingMap_bijective` 📖	mathematical	—	`Function.Bijective` `Function.Embedding` `DFunLike.coe` `AddActionHom` `Function.Embedding.vadd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom` `zeroEmbeddingMap`	—	`Equiv.bijective`

AlternatingGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	—	`MulAction.IsMultiplyPretransitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction` `Nat.card`	—	`alternatingGroup.isMultiplyPretransitive`
`isPreprimitive_of_three_le_card` 📖	mathematical	`Nat.card`	`MulAction.IsPreprimitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	—	`alternatingGroup.isPreprimitive_of_three_le_card`
`isPretransitive_of_three_le_card` 📖	mathematical	`Nat.card`	`MulAction.IsPretransitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	—	`alternatingGroup.isPretransitive_of_three_le_card`
`isTrivialBlock_of_isBlock` 📖	mathematical	`MulAction.IsBlock` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	`MulAction.IsTrivialBlock`	—	`alternatingGroup.isTrivialBlock_of_isBlock`

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_if_isMultiplyPretransitive` 📖	mathematical	—	`Top.top` `Subgroup` `Equiv.Perm` `permGroup` `Subgroup.instTop`	—	`eq_top_of_isMultiplyPretransitive`
`eq_top_of_isMultiplyPretransitive` 📖	mathematical	—	`Top.top` `Subgroup` `Equiv.Perm` `permGroup` `Subgroup.instTop`	—	`eq_top_iff` `MulAction.exists_smul_eq` `Nat.card_eq_fintype_card` `Function.Bijective.surjective` `Fintype.bijective_iff_injective_and_card` `EmbeddingLike.injective` `Function.instEmbeddingLikeEmbedding` `Fintype.card_fin` `Function.Embedding.ext_iff` `lt_or_eq_of_le` `Fin.prop` `lt_irrefl` `ext` `SetLike.coe_mem`
`instIsPreprimitive` 📖	mathematical	—	`MulAction.IsPreprimitive` `Equiv.Perm` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `MulAction.toSemigroupAction` `applyMulAction`	—	`MulAction.isPreprimitive_of_is_two_pretransitive` `isMultiplyPretransitive`
`isMultiplyPretransitive` 📖	mathematical	—	`MulAction.IsMultiplyPretransitive` `Equiv.Perm` `permGroup` `applyMulAction`	—	`MulAction.isMultiplyPretransitive_iff` `Cardinal.mk_fintype` `Fintype.card_ofFinset` `Finset.card_image_of_injective` `Function.instEmbeddingLikeEmbedding` `Fintype.card_plift` `Fintype.card_fin` `add_comm` `Cardinal.mk_sum_compl` `Cardinal.eq` `Function.Injective.extend_apply` `Function.Embedding.injective` `Set.mem_compl_iff` `Subtype.val_injective` `Function.extend_apply'` `Subtype.coe_prop` `Set.mem_range_self` `Equiv.injective` `Equiv.apply_symm_apply` `Function.Embedding.ext`

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addActionHom_embedding_isBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`Function.Embedding` `Function.Embedding.vadd` `Function.Injective.addActionHom_embedding` `injective`	—	`injective` `Function.Injective.addActionHom_embedding_isInjective` `Function.bijective_iff_has_inverse` `Function.RightInverse.injective` `EmbeddingLike.injective` `Function.instEmbeddingLikeEmbedding` `Function.Embedding.ext` `Function.Injective.addActionHom_embedding_apply`
`mulActionHom_embedding_isBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`Function.Embedding` `Function.Embedding.smul` `Function.Injective.mulActionHom_embedding` `injective`	—	`injective` `Function.Injective.mulActionHom_embedding_isInjective` `Function.bijective_iff_has_inverse` `Function.RightInverse.injective` `EmbeddingLike.injective` `Function.instEmbeddingLikeEmbedding` `Function.Embedding.ext` `Function.Injective.mulActionHom_embedding_apply`

Function.Injective

Definitions

Name	Category	Theorems
`addActionHom_embedding` 📖	CompOp	3 math math: `Function.Bijective.addActionHom_embedding_isBijective`, `addActionHom_embedding_isInjective`, `addActionHom_embedding_apply`
`mulActionHom_embedding` 📖	CompOp	3 math math: `mulActionHom_embedding_apply`, `mulActionHom_embedding_isInjective`, `Function.Bijective.mulActionHom_embedding_isBijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addActionHom_embedding_apply` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.vadd` `addActionHom_embedding`	—	—
`addActionHom_embedding_isInjective` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`Function.Embedding` `Function.Embedding.vadd` `addActionHom_embedding`	—	`Function.Embedding.ext` `addActionHom_embedding_apply`
`mulActionHom_embedding_apply` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.smul` `mulActionHom_embedding`	—	—
`mulActionHom_embedding_isInjective` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`Function.Embedding` `Function.Embedding.smul` `mulActionHom_embedding`	—	`Function.Embedding.ext` `mulActionHom_embedding_apply`

IsMultiplyPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alternatingGroup_le` 📖	mathematical	—	`Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `alternatingGroup`	—	`alternatingGroup.eq_bot_of_card_le_two` `LT.lt.le` `Nat.card_eq_fintype_card` `bot_le` `Equiv.Perm.alternatingGroup_le_of_index_le_two` `Set.exists_subset_card_eq` `Set.ncard_univ` `MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul` `Finite.of_fintype` `mul_le_mul_iff_of_pos_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.card_pos` `One.instNonempty` `Subgroup.instFiniteSubtypeMem` `Equiv.finite_left` `Subgroup.card_mul_index` `Subgroup.index_mul_card` `mul_assoc` `mul_comm` `Nat.factorial_two` `Nat.card_perm`

MulAction

Definitions

Name	Category	Theorems
`IsMultiplyPretransitive` 📖	MathDef	20 math math: `IsPreprimitive.is_two_pretransitive`, `SubMulAction.ofStabilizer.isMultiplyPretransitive_iff`, `Equiv.Perm.isMultiplyPretransitive_of_nontrivial`, `IsMultiplyPreprimitive.isMultiplyPretransitive`, `SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj`, `SubMulAction.ofFixingSubgroup.isMultiplyPretransitive`, `isMultiplyPreprimitive_iff`, `AlternatingGroup.isMultiplyPretransitive`, `instIsMultiplyPretransitiveOfIsMultiplyPreprimitive`, `is_two_pretransitive_iff`, `SubMulAction.ofStabilizer.isMultiplyPretransitive`, `IsPreprimitive.is_two_motive_of_is_motive`, `isMultiplyPretransitive_iff`, `alternatingGroup.isMultiplyPretransitive`, `SubMulAction.ofFixingSubgroup.isMultiplyPretransitive'`, `is_zero_pretransitive'`, `isMultiplyPretransitive_of_le'`, `is_one_pretransitive_iff`, `isMultiplyPretransitive_of_le`, `Equiv.Perm.isMultiplyPretransitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `Function.Embedding` `Function.Embedding.smul`	—	`isPretransitive_iff`
`isMultiplyPretransitive_of_le` 📖	mathematical	`Nat.card`	`IsMultiplyPretransitive`	—	`IsPretransitive.of_surjective_map` `Fin.Embedding.restrictSurjective_of_add_le_natCard`
`isMultiplyPretransitive_of_le'` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`IsMultiplyPretransitive`	—	`IsPretransitive.of_surjective_map` `Fin.Embedding.restrictSurjective_of_add_le_ENatCard`
`isPreprimitive_of_is_two_pretransitive` 📖	mathematical	—	`IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`isPretransitive_of_is_two_pretransitive` `Set.subsingleton_or_nontrivial` `Set.top_eq_univ` `eq_top_iff` `is_two_pretransitive_iff` `isBlock_iff_smul_eq_of_mem` `Set.smul_mem_smul_set`
`isPretransitive_of_is_two_pretransitive` 📖	mathematical	—	`IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`one_smul` `is_two_pretransitive_iff`
`is_one_pretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`oneEmbedding_isPretransitive_iff`
`is_two_pretransitive_iff` 📖	mathematical	—	`IsMultiplyPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`exists_smul_eq` `Function.Embedding.embFinTwo_apply_zero` `Function.Embedding.smul_apply` `Function.Embedding.embFinTwo_apply_one` `Function.Embedding.injective` `Function.Embedding.ext` `Fin.eq_one_of_ne_zero`
`is_zero_pretransitive` 📖	mathematical	—	`IsPretransitive` `Function.Embedding` `Function.Embedding.smul`	—	`instIsPretransitiveOfSubsingleton` `Unique.instSubsingleton`
`is_zero_pretransitive'` 📖	mathematical	—	`IsMultiplyPretransitive`	—	`instIsPretransitiveOfSubsingleton` `Unique.instSubsingleton` `Fin.isEmpty'`
`oneEmbedding_isPretransitive_iff` 📖	mathematical	—	`IsPretransitive` `Function.Embedding` `Function.Embedding.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`isPretransitive_congr` `MulActionHom.oneEmbeddingMap_bijective`

MulAction.IsMultiplyPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`index_of_fixingSubgroup_eq` 📖	mathematical	—	`Subgroup.index` `fixingSubgroup` `Nat.choose` `Nat.card` `Set.ncard` `Nat.factorial`	—	`Nat.factorial_pos` `index_of_fixingSubgroup_mul` `Nat.choose_mul_factorial_mul_factorial` `Set.ncard_univ` `Set.ncard_le_ncard` `Set.subset_univ` `Set.toFinite` `Subtype.finite`
`index_of_fixingSubgroup_mul` 📖	mathematical	`Set.ncard`	`Subgroup.index` `fixingSubgroup` `Nat.factorial` `Nat.card`	—	`Set.ncard_eq_zero` `Set.toFinite` `Subtype.finite` `fixingSubgroup_empty` `Subgroup.index_top` `tsub_zero` `Nat.instOrderedSub` `one_mul` `MulAction.is_one_pretransitive_iff` `MulAction.isMultiplyPretransitive_of_le` `Set.ncard_univ` `Set.ncard_le_ncard` `Set.subset_univ` `Set.finite_univ` `Set.ncard_pos` `Set.image_preimage_eq_inter_range` `Subtype.range_coe_subtype` `Set.diff_eq_compl_inter` `Set.inter_comm` `Set.insert_diff_singleton` `Set.insert_eq_of_mem` `SubMulAction.fixingSubgroup_of_insert` `Subgroup.index_map` `MonoidHom.ker_eq_bot_iff` `sup_bot_eq` `Subgroup.range_subtype` `Set.ncard_image_of_injective` `Subtype.coe_injective` `Set.ncard_insert_of_notMem` `Finite.Set.finite_image` `SubMulAction.nat_card_ofStabilizer_eq` `SubMulAction.ofStabilizer.isMultiplyPretransitive` `add_comm` `mul_comm` `MulAction.index_stabilizer_of_transitive` `Nat.mul_factorial_pred` `Nat.card_ne_zero`

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_embedding` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`MulAction.IsPretransitive` `Function.Embedding` `Function.Embedding.smul`	—	`Function.surjInv_eq` `exists_smul_eq` `Function.Embedding.ext` `Function.Embedding.smul_apply` `DFunLike.ext_iff` `MulActionHom.map_smul'`
`of_embedding_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`MulAction.IsPretransitive` `Function.Embedding` `Function.Embedding.smul`	—	`MulAction.isPretransitive_congr` `Function.Bijective.injective` `Function.Bijective.mulActionHom_embedding_isBijective`

MulActionHom

Definitions

Name	Category	Theorems
`embMap` 📖	CompOp	—
`oneEmbeddingMap` 📖	CompOp	1 math math: `oneEmbeddingMap_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`oneEmbeddingMap_bijective` 📖	mathematical	—	`Function.Bijective` `Function.Embedding` `DFunLike.coe` `MulActionHom` `Function.Embedding.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom` `oneEmbeddingMap`	—	`Equiv.bijective`

SubAddAction.ofFixingAddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	`Set.ncard`	`AddAction.IsMultiplyPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `fixingAddSubgroup` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofFixingAddSubgroup` `SubAddAction.addAction`	—	`Finite.card_eq` `Finite.of_fintype` `Nat.card_eq_fintype_card` `Fintype.card_fin` `AddAction.exists_vadd_eq` `Equiv.apply_symm_apply` `append_left` `Function.Embedding.vadd_apply` `Function.Embedding.ext` `SubAddAction.instVAddMemClass` `SetLike.val_vadd` `AddSubgroup.mk_vadd` `append_right`
`isMultiplyPretransitive'` 📖	mathematical	`Set.ncard` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`AddAction.IsMultiplyPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `fixingAddSubgroup` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofFixingAddSubgroup` `SubAddAction.addAction`	—	`isMultiplyPretransitive` `AddAction.isMultiplyPretransitive_of_le'`

SubAddAction.ofStabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	—	`AddAction.IsMultiplyPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofStabilizer` `SubAddAction.addAction`	—	`AddAction.exists_vadd_eq` `AddAction.mem_stabilizer_iff` `snoc_last` `DFunLike.ext_iff` `Function.Embedding.ext` `snoc_castSucc` `Function.Embedding.vadd_apply` `SubAddAction.exists_vadd_of_last_eq` `AddAction.IsPretransitive.exists_vadd_eq` `AddSemigroupAction.add_vadd` `neg_vadd_eq_iff` `Fin.eq_castSucc_or_eq_last` `Subtype.prop`
`isMultiplyPretransitive_iff` 📖	mathematical	—	`AddAction.IsMultiplyPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofStabilizer` `SubAddAction.addAction`	—	`AddAction.exists_vadd_eq` `isMultiplyPretransitive_iff_of_conj`
`isMultiplyPretransitive_iff_of_conj` 📖	mathematical	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`AddAction.IsMultiplyPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `SubAddAction` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofStabilizer` `SubAddAction.addAction`	—	`AddAction.IsPretransitive.of_embedding_congr` `AddEquiv.surjective` `conjMap_bijective`
`isPretransitive_iff` 📖	mathematical	—	`AddAction.IsPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `SubAddAction` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofStabilizer` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`VAddAssocClass.left` `AddAction.exists_vadd_eq` `isPretransitive_iff_of_conj`
`isPretransitive_iff_of_conj` 📖	mathematical	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	`AddAction.IsPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddAction.stabilizer` `SubAddAction` `AddSubgroup.toAddGroup` `AddSubgroup.instAddAction` `SubAddAction.instSetLike` `SubAddAction.ofStabilizer` `SubAddAction.vadd'` `AddMonoid.toAddAction` `VAddAssocClass.left`	—	`AddAction.isPretransitive_congr` `AddEquiv.surjective` `conjMap_bijective`

SubMulAction.ofFixingSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	`Set.ncard`	`MulAction.IsMultiplyPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `fixingSubgroup` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofFixingSubgroup` `SubMulAction.mulAction`	—	`Finite.card_eq` `Finite.of_fintype` `Nat.card_eq_fintype_card` `Fintype.card_fin` `MulAction.exists_smul_eq` `Equiv.apply_symm_apply` `append_left` `Function.Embedding.smul_apply` `Function.Embedding.ext` `SubMulAction.instSMulMemClass` `SetLike.val_smul` `Subgroup.mk_smul`
`isMultiplyPretransitive'` 📖	mathematical	`Set.ncard` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `ENat.card`	`MulAction.IsMultiplyPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `fixingSubgroup` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofFixingSubgroup` `SubMulAction.mulAction`	—	`isMultiplyPretransitive` `MulAction.isMultiplyPretransitive_of_le'`

SubMulAction.ofStabilizer

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	—	`MulAction.IsMultiplyPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofStabilizer` `SubMulAction.mulAction`	—	`MulAction.exists_smul_eq` `snoc_last` `DFunLike.ext_iff` `Function.Embedding.ext` `snoc_castSucc` `Function.Embedding.smul_apply` `SubMulAction.exists_smul_of_last_eq` `MulAction.IsPretransitive.exists_smul_eq` `SemigroupAction.mul_smul` `Fin.eq_castSucc_or_eq_last` `Subtype.prop`
`isMultiplyPretransitive_iff` 📖	mathematical	—	`MulAction.IsMultiplyPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofStabilizer` `SubMulAction.mulAction`	—	`MulAction.exists_smul_eq` `isMultiplyPretransitive_iff_of_conj`
`isMultiplyPretransitive_iff_of_conj` 📖	mathematical	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MulAction.IsMultiplyPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `SubMulAction` `Subgroup.toGroup` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofStabilizer` `SubMulAction.mulAction`	—	`MulAction.IsPretransitive.of_embedding_congr` `MulEquiv.surjective` `conjMap_bijective`
`isPretransitive_iff` 📖	mathematical	—	`MulAction.IsPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `SubMulAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofStabilizer` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`IsScalarTower.left` `MulAction.exists_smul_eq` `isPretransitive_iff_of_conj`
`isPretransitive_iff_of_conj` 📖	mathematical	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	`MulAction.IsPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MulAction.stabilizer` `SubMulAction` `Subgroup.toGroup` `Subgroup.instMulAction` `SubMulAction.instSetLike` `SubMulAction.ofStabilizer` `SubMulAction.smul'` `Monoid.toMulAction` `IsScalarTower.left`	—	`MulAction.isPretransitive_congr` `MulEquiv.surjective` `conjMap_bijective`

alternatingGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMultiplyPretransitive` 📖	mathematical	—	`MulAction.IsMultiplyPretransitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction` `Nat.card`	—	`lt_or_ge` `le_of_lt` `MulAction.is_zero_pretransitive` `Fin.isEmpty'` `Equiv.Perm.isMultiplyPretransitive` `MulAction.isMultiplyPretransitive_of_le` `le_rfl` `Finite.of_fintype` `MulAction.exists_smul_eq` `Int.units_eq_one_or` `Finset.card_compl` `Finset.card_image_of_injective` `Function.Embedding.inj'` `Finset.card_univ` `Nat.card_eq_fintype_card` `Fintype.card_fin` `tsub_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Finset.card_eq_two` `Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap'` `mul_neg` `mul_one` `neg_neg` `Function.Embedding.ext` `Finset.mem_image` `Finset.mem_univ` `Equiv.swap_apply_of_ne_of_ne` `Finset.mem_singleton` `Finset.mem_insert` `Finset.notMem_compl`
`isPreprimitive_of_three_le_card` 📖	mathematical	`Nat.card`	`MulAction.IsPreprimitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	—	`isPretransitive_of_three_le_card` `isTrivialBlock_of_isBlock`
`isPretransitive_of_three_le_card` 📖	mathematical	`Nat.card`	`MulAction.IsPretransitive` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	—	`MulAction.is_one_pretransitive_iff` `MulAction.isMultiplyPretransitive_of_le` `isMultiplyPretransitive` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_trans` `Mathlib.Meta.NormNum.isNat_le_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Finite.of_fintype`
`isTrivialBlock_of_isBlock` 📖	mathematical	`MulAction.IsBlock` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction` `Equiv.Perm.applyMulAction`	`MulAction.IsTrivialBlock`	—	`le_or_gt` `MulAction.isTrivialBlock_of_card_le_two` `Finite.of_fintype` `le_antisymm` `isPretransitive_of_three_le_card` `Eq.ge` `MulAction.IsPreprimitive.of_prime_card` `Nat.prime_three` `MulAction.IsPreprimitive.isTrivialBlock_of_isBlock` `MulAction.isPreprimitive_of_is_two_pretransitive` `MulAction.isMultiplyPretransitive_of_le` `isMultiplyPretransitive` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_of_lt`

---

← Back to Index