Documentation Verification Report

Primitive

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

Statistics

Metric	Count
Definitions `IsPreprimitive`, `IsQuasiPreprimitive`, `IsPreprimitive`, `IsQuasiPreprimitive`	4
Theorems `subsingleton_or_eq_univ`, `exists_mem_vadd_and_notMem_vadd`, `isCoatom_stabilizer_of_isPreprimitive`, `isQuasiPreprimitive`, `isTrivialBlock_of_isBlock`, `mk'`, `of_card_lt`, `of_isTrivialBlock_base`, `of_isTrivialBlock_of_notMem_fixedPoints`, `of_prime_card`, `of_subsingleton`, `of_surjective`, `toIsPretransitive`, `isPretransitive_of_normal`, `toIsPretransitive`, `isCoatom_stabilizer_iff_preprimitive`, `isPreprimitive_congr`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `subsingleton_or_eq_univ`, `exists_mem_smul_and_notMem_smul`, `isCoatom_stabilizer_of_isPreprimitive`, `isQuasiPreprimitive`, `isTrivialBlock_of_isBlock`, `mk'`, `of_card_lt`, `of_isTrivialBlock_base`, `of_isTrivialBlock_of_notMem_fixedPoints`, `of_prime_card`, `of_subsingleton`, `of_surjective`, `toIsPretransitive`, `isPretransitive_of_normal`, `toIsPretransitive`, `isCoatom_stabilizer_iff_preprimitive`, `isPreprimitive_congr`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `isTrivialBlock_of_card_le_two`	37
Total	41

AddAction

Definitions

Name	Category	Theorems
`IsPreprimitive` 📖	CompData	17 math math: `IsPreprimitive.of_isTrivialBlock_base`, `isPreprimitive_ofFixingAddSubgroup_conj_iff`, `IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints`, `IsPreprimitive.of_surjective`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `is_zero_preprimitive_iff`, `isPreprimitive_congr`, `isPreprimitive_of_is_two_pretransitive`, `isMultiplyPreprimitive_iff`, `IsMultiplyPreprimitive.isPreprimitive_ofFixingAddSubgroup`, `IsPreprimitive.mk'`, `IsPreprimitive.of_subsingleton`, `IsPreprimitive.of_prime_card`, `isPreprimitive_fixingAddSubgroup_insert_iff`, `isCoatom_stabilizer_iff_preprimitive`, `isPreprimitive_of_fixingAddSubgroup_empty_iff`, `IsPreprimitive.of_card_lt`
`IsQuasiPreprimitive` 📖	CompData	1 math math: `IsPreprimitive.isQuasiPreprimitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoatom_stabilizer_iff_preprimitive` 📖	mathematical	—	`IsCoatom` `AddSubgroup` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `AddSubgroup.instCompleteLattice` `stabilizer` `IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`isSimpleOrder_blockMem_iff_isPreprimitive` `Set.isSimpleOrder_Ici_iff_isCoatom` `isSimpleOrder_iff_isCoatom_bot` `OrderIso.isCoatom_iff` `OrderIso.map_bot`
`isPreprimitive_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `instFunLikeAddActionHom`	`IsPreprimitive`	—	`IsPreprimitive.of_surjective` `Function.Bijective.surjective` `isPretransitive_congr` `IsPreprimitive.toIsPretransitive` `Set.preimage_image_eq` `Function.Bijective.injective` `IsTrivialBlock.preimage` `IsPreprimitive.isTrivialBlock_of_isBlock` `IsBlock.image`
`isSimpleOrder_blockMem_iff_isPreprimitive` 📖	mathematical	—	`IsSimpleOrder` `BlockMem` `Set` `Set.instLE` `Set.instMembership` `IsBlock` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `BlockMem.instBoundedOrder` `IsPreprimitive`	—	`IsSimpleOrder.eq_bot_or_eq_top` `IsPreprimitive.of_isTrivialBlock_base` `Set.subsingleton_singleton` `BlockMem.instNontrivial` `IsPreprimitive.isTrivialBlock_of_isBlock` `Set.Subsingleton.eq_singleton_of_mem` `Set.singleton_ne_univ`

AddAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_or_eq_univ` 📖	mathematical	`AddAction.IsBlock`	`Set.Subsingleton` `Set.univ`	—	`AddAction.IsPreprimitive.isTrivialBlock_of_isBlock`

AddAction.IsPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_vadd_and_notMem_vadd` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`isTrivialBlock_of_isBlock` `AddAction.IsBlock.of_subset` `AddAction.IsQuasiPreprimitive.toIsPretransitive` `isQuasiPreprimitive` `Set.Subsingleton.eq_singleton_of_mem` `Set.mem_iInter` `AddAction.exists_vadd_eq` `Set.biInter_subset_of_mem` `eq_neg_vadd_iff` `Set.univ_subset_iff` `Set.vadd_set_univ` `Set.mem_singleton_iff`
`isCoatom_stabilizer_of_isPreprimitive` 📖	mathematical	—	`IsCoatom` `AddSubgroup` `PartialOrder.toPreorder` `AddSubgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `AddSubgroup.instCompleteLattice` `AddAction.stabilizer`	—	`AddAction.isCoatom_stabilizer_iff_preprimitive` `toIsPretransitive`
`isQuasiPreprimitive` 📖	mathematical	—	`AddAction.IsQuasiPreprimitive`	—	`toIsPretransitive` `Set.ne_univ_iff_exists_notMem` `AddAction.isPretransitive_iff_orbit_eq_univ` `isTrivialBlock_of_isBlock` `AddAction.IsBlock.orbit_of_normal` `AddAction.mem_fixedPoints` `Set.mem_singleton_iff` `Set.ext` `Set.Subsingleton.eq_singleton_of_mem` `AddAction.mem_orbit_self`
`isTrivialBlock_of_isBlock` 📖	mathematical	`AddAction.IsBlock`	`AddAction.IsTrivialBlock`	—	—
`mk'` 📖	mathematical	`AddAction.IsTrivialBlock`	`AddAction.IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.ne_univ_iff_exists_notMem` `of_isTrivialBlock_of_notMem_fixedPoints`
`of_card_lt` 📖	mathematical	`Nat.card` `Set.ncard` `Set.range` `DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`AddAction.IsPreprimitive`	—	`Set.eq_empty_or_nonempty` `Set.subsingleton_empty` `AddAction.IsTrivialBlock.eq_1` `lt_of_mul_lt_mul_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `lt_of_le_of_lt` `AddAction.IsBlock.ncard_block_add_ncard_orbit_eq` `Subtype.finite` `Set.instFinite` `Setoid.IsPartition.ncard_eq_finsum` `AddAction.IsBlock.isBlockSystem` `Set.toFinite` `finsum_eq_sum_of_fintype` `le_trans` `Finset.sum_le_card_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Set.image_preimage_eq_range_inter` `Set.Subsingleton.image` `isTrivialBlock_of_isBlock` `AddAction.IsBlock.preimage` `AddAction.IsBlock.translate` `AddAction.IsBlock.eq_univ_of_card_lt` `lt_of_lt_of_le` `mul_comm` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.succ_pos'` `Set.ncard_le_ncard` `Set.preimage_eq_univ_iff` `Set.ncard_image_le` `Set.ncard_le_one_iff_subsingleton` `Finite.Set.finite_inter_of_left` `nsmul_one` `Finset.card_univ` `Set.toFinset_card` `Set.ncard_eq_toFinset_card'` `AddAction.orbit.eq_1` `Nat.cast_id` `le_refl` `zero_le` `Nat.instCanonicallyOrderedAdd`
`of_isTrivialBlock_base` 📖	mathematical	`AddAction.IsTrivialBlock`	`AddAction.IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Set.eq_empty_or_nonempty` `Set.subsingleton_empty` `AddAction.exists_vadd_eq` `AddAction.IsTrivialBlock.vadd_iff` `AddAction.IsBlock.translate`
`of_isTrivialBlock_of_notMem_fixedPoints` 📖	mathematical	`Set` `Set.instMembership` `AddAction.fixedPoints` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.IsTrivialBlock`	`AddAction.IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction`	—	`AddAction.isPretransitive_iff_base` `AddAction.mem_orbit_self` `AddAction.IsBlock.orbit` `AddAction.mem_fixedPoints` `Set.mem_singleton_iff` `Set.subsingleton_iff_singleton` `AddAction.mem_orbit` `AddAction.mem_orbit_iff` `Set.mem_univ` `Set.eq_empty_or_nonempty` `Set.subsingleton_empty` `AddAction.exists_vadd_eq` `AddAction.IsTrivialBlock.vadd_iff` `AddAction.IsBlock.translate`
`of_prime_card` 📖	mathematical	`Nat.Prime` `Nat.card`	`AddAction.IsPreprimitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	`Nat.card_ne_zero` `Nat.Prime.ne_zero` `Set.eq_univ_iff_ncard` `Nat.Prime.dvd_iff_eq` `LT.lt.ne'` `Set.one_lt_ncard` `Set.toFinite` `Subtype.finite` `AddAction.IsBlock.ncard_dvd_card` `Set.Nontrivial.nonempty` `Set.subsingleton_or_nontrivial`
`of_subsingleton` 📖	mathematical	—	`AddAction.IsPreprimitive`	—	`Set.subsingleton_of_subsingleton`
`of_surjective` 📖	mathematical	`DFunLike.coe` `AddActionHom` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instFunLikeAddActionHom`	`AddAction.IsPreprimitive`	—	`AddAction.IsPretransitive.of_surjective_map` `toIsPretransitive` `Set.image_preimage_eq` `AddAction.IsTrivialBlock.image` `isTrivialBlock_of_isBlock` `AddAction.IsBlock.preimage`
`toIsPretransitive` 📖	mathematical	—	`AddAction.IsPretransitive`	—	—

AddAction.IsQuasiPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_of_normal` 📖	mathematical	—	`AddAction.IsPretransitive` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddSubgroup.instAddAction`	—	—
`toIsPretransitive` 📖	mathematical	—	`AddAction.IsPretransitive` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction`	—	—

MulAction

Definitions

Name	Category	Theorems
`IsPreprimitive` 📖	CompData	28 math math: `IsPreprimitive.of_isTrivialBlock_of_notMem_fixedPoints`, `IsPreprimitive.of_surjective`, `isPreprimitive_of_fixingSubgroup_empty_iff`, `IsPreprimitive.of_card_lt`, `alternatingGroup.isPreprimitive_of_three_le_card`, `isPreprimitive_of_is_two_pretransitive`, `is_one_preprimitive_iff`, `AlternatingGroup.isPreprimitive_of_three_le_card`, `isPreprimitive_ofFixingSubgroup_conj_iff`, `isCoatom_stabilizer_iff_preprimitive`, `Equiv.Perm.stabilizer_isPreprimitive`, `isPreprimitive_fixingSubgroup_insert_iff`, `isPreprimitive_stabilizer_subgroup`, `IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup`, `IsPreprimitive.of_prime_card`, `isMultiplyPreprimitive_iff`, `IsPreprimitive.of_isTrivialBlock_base`, `isSimpleOrder_blockMem_iff_isPreprimitive`, `Equiv.Perm.instIsPreprimitive`, `alternatingGroup.stabilizer_isPreprimitive`, `isPreprimitive_stabilizer_of_surjective`, `Set.powersetCard.isPreprimitive_perm`, `Set.powersetCard.isPreprimitive_alternatingGroup`, `IsPreprimitive.mk'`, `SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter`, `isPreprimitive_congr`, `alternatingGroup.stabilizer_subgroup_isPreprimitive`, `IsPreprimitive.of_subsingleton`
`IsQuasiPreprimitive` 📖	CompData	1 math math: `IsPreprimitive.isQuasiPreprimitive`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoatom_stabilizer_iff_preprimitive` 📖	mathematical	—	`IsCoatom` `Subgroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `stabilizer` `IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`isSimpleOrder_blockMem_iff_isPreprimitive` `Set.isSimpleOrder_Ici_iff_isCoatom` `OrderIso.isCoatom_iff` `OrderIso.map_bot`
`isPreprimitive_congr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `instFunLikeMulActionHom`	`IsPreprimitive`	—	`IsPreprimitive.of_surjective` `Function.Bijective.surjective` `isPretransitive_congr` `IsPreprimitive.toIsPretransitive` `Set.preimage_image_eq` `Function.Bijective.injective` `IsTrivialBlock.preimage` `IsPreprimitive.isTrivialBlock_of_isBlock` `IsBlock.image`
`isSimpleOrder_blockMem_iff_isPreprimitive` 📖	mathematical	—	`IsSimpleOrder` `BlockMem` `Set` `Set.instLE` `Set.instMembership` `IsBlock` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `BlockMem.instBoundedOrder` `IsPreprimitive`	—	`IsSimpleOrder.eq_bot_or_eq_top` `IsPreprimitive.of_isTrivialBlock_base` `Set.subsingleton_singleton` `BlockMem.instNontrivial` `IsPreprimitive.isTrivialBlock_of_isBlock` `Set.Subsingleton.eq_singleton_of_mem`
`isTrivialBlock_of_card_le_two` 📖	mathematical	`Nat.card`	`IsTrivialBlock`	—	`IsTrivialBlock.eq_1` `Set.ncard_le_one_iff_subsingleton` `Subtype.finite` `Set.eq_univ_iff_ncard` `Set.ncard_le_card`

MulAction.IsBlock

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_or_eq_univ` 📖	mathematical	`MulAction.IsBlock`	`Set.Subsingleton` `Set.univ`	—	`MulAction.IsPreprimitive.isTrivialBlock_of_isBlock`

MulAction.IsPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_smul_and_notMem_smul` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`isTrivialBlock_of_isBlock` `MulAction.IsBlock.of_subset` `MulAction.IsQuasiPreprimitive.toIsPretransitive` `isQuasiPreprimitive` `Set.Subsingleton.eq_singleton_of_mem` `Set.mem_iInter` `MulAction.exists_smul_eq` `Set.biInter_subset_of_mem` `eq_inv_smul_iff` `Set.univ_subset_iff` `Set.smul_set_univ` `Set.mem_singleton_iff`
`isCoatom_stabilizer_of_isPreprimitive` 📖	mathematical	—	`IsCoatom` `Subgroup` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `BoundedOrder.toOrderTop` `Preorder.toLE` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice` `MulAction.stabilizer`	—	`MulAction.isCoatom_stabilizer_iff_preprimitive` `toIsPretransitive`
`isQuasiPreprimitive` 📖	mathematical	—	`MulAction.IsQuasiPreprimitive`	—	`toIsPretransitive` `Set.ne_univ_iff_exists_notMem` `MulAction.isPretransitive_iff_orbit_eq_univ` `isTrivialBlock_of_isBlock` `MulAction.IsBlock.orbit_of_normal` `Set.mem_singleton_iff` `Set.ext` `Set.Subsingleton.eq_singleton_of_mem` `MulAction.mem_orbit_self`
`isTrivialBlock_of_isBlock` 📖	mathematical	`MulAction.IsBlock`	`MulAction.IsTrivialBlock`	—	—
`mk'` 📖	mathematical	`MulAction.IsTrivialBlock`	`MulAction.IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`of_isTrivialBlock_of_notMem_fixedPoints`
`of_card_lt` 📖	mathematical	`Nat.card` `Set.ncard` `Set.range` `DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`MulAction.IsPreprimitive`	—	`Set.eq_empty_or_nonempty` `MulAction.IsTrivialBlock.eq_1` `lt_of_mul_lt_mul_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `lt_of_le_of_lt` `MulAction.IsBlock.ncard_block_mul_ncard_orbit_eq` `Subtype.finite` `Set.instFinite` `Setoid.IsPartition.ncard_eq_finsum` `MulAction.IsBlock.isBlockSystem` `Set.toFinite` `finsum_eq_sum_of_fintype` `le_trans` `Finset.sum_le_card_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Set.image_preimage_eq_range_inter` `Set.Subsingleton.image` `isTrivialBlock_of_isBlock` `MulAction.IsBlock.preimage` `MulAction.IsBlock.translate` `MulAction.IsBlock.eq_univ_of_card_lt` `lt_of_lt_of_le` `mul_comm` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.succ_pos'` `Set.ncard_le_ncard` `Set.ncard_image_le` `Finite.Set.finite_inter_of_left` `nsmul_one` `Finset.card_univ` `Set.toFinset_card` `Set.ncard_eq_toFinset_card'` `MulAction.orbit.eq_1` `Nat.cast_id` `le_refl` `zero_le` `Nat.instCanonicallyOrderedAdd`
`of_isTrivialBlock_base` 📖	mathematical	`MulAction.IsTrivialBlock`	`MulAction.IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Set.eq_empty_or_nonempty` `MulAction.exists_smul_eq` `MulAction.IsTrivialBlock.smul_iff` `MulAction.IsBlock.translate`
`of_isTrivialBlock_of_notMem_fixedPoints` 📖	mathematical	`Set` `Set.instMembership` `MulAction.fixedPoints` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.IsTrivialBlock`	`MulAction.IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`MulAction.isPretransitive_iff_base` `MulAction.mem_orbit_self` `MulAction.IsBlock.orbit` `Set.mem_singleton_iff` `Set.subsingleton_iff_singleton` `MulAction.mem_orbit` `MulAction.mem_orbit_iff` `Set.mem_univ` `Set.eq_empty_or_nonempty` `MulAction.exists_smul_eq` `MulAction.IsTrivialBlock.smul_iff` `MulAction.IsBlock.translate`
`of_prime_card` 📖	mathematical	`Nat.Prime` `Nat.card`	`MulAction.IsPreprimitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	`Nat.card_ne_zero` `Nat.Prime.ne_zero` `Set.eq_univ_iff_ncard` `Nat.Prime.dvd_iff_eq` `LT.lt.ne'` `Set.one_lt_ncard` `Set.toFinite` `Subtype.finite` `MulAction.IsBlock.ncard_dvd_card` `Set.Nontrivial.nonempty` `Set.subsingleton_or_nontrivial`
`of_subsingleton` 📖	mathematical	—	`MulAction.IsPreprimitive`	—	`Set.subsingleton_of_subsingleton`
`of_surjective` 📖	mathematical	`DFunLike.coe` `MulActionHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `instFunLikeMulActionHom`	`MulAction.IsPreprimitive`	—	`MulAction.IsPretransitive.of_surjective_map` `toIsPretransitive` `Set.image_preimage_eq` `MulAction.IsTrivialBlock.image` `isTrivialBlock_of_isBlock` `MulAction.IsBlock.preimage`
`toIsPretransitive` 📖	mathematical	—	`MulAction.IsPretransitive`	—	—

MulAction.IsQuasiPreprimitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPretransitive_of_normal` 📖	mathematical	—	`MulAction.IsPretransitive` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subgroup.toGroup` `MulAction.toSemigroupAction` `Subgroup.instMulAction`	—	—
`toIsPretransitive` 📖	mathematical	—	`MulAction.IsPretransitive` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction`	—	—

---

← Back to Index