📁 Source: Mathlib/GroupTheory/GroupAction/Jordan.lean
alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem
eq_top_of_isPreprimitive_of_isSwap_mem
isMultiplyPretransitive_of_nontrivial
isPretransitive_of_isCycle_mem
subgroup_eq_top_of_isPreprimitive_of_isSwap_mem
subgroup_eq_top_of_nontrivial
isMultiplyPreprimitive
is_two_motive_of_is_motive
is_two_preprimitive
is_two_pretransitive
normalClosure_of_stabilizer_eq_top
IsThreeCycle
Equiv.Perm
Subgroup
permGroup
SetLike.instMembership
Subgroup.instSetLike
Preorder.toLE
PartialOrder.toPreorder
Subgroup.instPartialOrder
alternatingGroup
alternatingGroup_le_of_index_le_two
Nat.card_pos
One.instNonempty
Subgroup.instFiniteSubtypeMem
Equiv.finite_left
Finite.of_fintype
Subgroup.index_mul_card
Nat.card_perm
le_trans
Nat.factorial_le
zero_add
mul_one
IsOrderedRing.toPosMulMono
IsStrictOrderedRing.toIsOrderedRing
Nat.instIsStrictOrderedRing
PosMulStrictMono.toPosMulReflectLE
LinearOrderedCommMonoidWithZero.toPosMulStrictMono
IsThreeCycle.orderOf
Nat.card_eq_fintype_card
orderOf_dvd_card
IsMultiplyPretransitive.alternatingGroup_le
MulAction.IsPreprimitive.isMultiplyPreprimitive
Set.ncard_add_ncard_compl
Set.toFinite
Subtype.finite
Set.ncard_coe_finset
IsThreeCycle.card_support
add_comm
IsScalarTower.left
IsThreeCycle.isCycle
MulAction.IsPreprimitive.of_prime_card
Fintype.card_subtype
Finset.ext
Finset.filter.congr_simp
Nat.prime_three
MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive
IsSwap
Top.top
Subgroup.instTop
Nat.card
MulAction.IsMultiplyPretransitive
finite_or_infinite
Nat.card_eq_zero_of_infinite
Nat.instCharZero
Nat.instAtLeastTwoHAddOfNat
Function.bijective_id
MonoidHom.range_eq_top
Subgroup.eq_top_of_card_eq
le_antisymm
Subgroup.card_le_card_group
Set.eq_univ_of_univ_subset
map_one
MonoidHomClass.toOneHomClass
MonoidHom.instMonoidHomClass
one_smul
MulAction.IsPretransitive.of_embedding_congr
isMultiplyPretransitive
MulAction.isMultiplyPretransitive_of_le'
ENat.card_eq_coe_fintype_card
not_nonempty_iff
Function.Embedding.nonempty_iff_card_le
Fintype.card_fin
MulAction.instIsPretransitiveOfSubsingleton
IsEmpty.instSubsingleton
IsCycle
MulAction.IsPretransitive
Subgroup.toGroup
fixingSubgroup
Subgroup.instMulAction
applyMulAction
Compl.compl
Set
Set.instCompl
SetLike.coe
Finset
Finset.instSetLike
support
SubMulAction
SemigroupAction.toSMul
Monoid.toSemigroup
DivInvMonoid.toMonoid
Group.toDivInvMonoid
MulAction.toSemigroupAction
SubMulAction.instSetLike
SubMulAction.ofFixingSubgroup
SubMulAction.smul'
Monoid.toMulAction
mem_fixingSubgroup_iff
MulAction.isPretransitive_iff
SetLike.coe_eq_coe
smul_smul
inv_mul_cancel_right
Fintype.card_subtype_le
Nat.factorial_two
Fintype.card_pos
IsSwap.orderOf
orderOf_submonoid
card_support_eq_two
eq_top_of_isMultiplyPretransitive
IsSwap.isCycle
Finset.coe_filter
Nat.prime_two
Subgroup.eq_top_of_le_card
LE.le.trans
Subgroup.one_lt_card_iff_ne_bot
Subgroup.nontrivial_iff_ne_bot
Set.ncard
MulAction.IsMultiplyPreprimitive
Nat.instCanonicallyOrderedAdd
Set.ncard_pos
Set.ext
Set.mem_image
Subtype.prop
Set.mem_singleton
MulAction.is_one_preprimitive_iff
MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer
MulAction.IsQuasiPreprimitive.toIsPretransitive
isQuasiPreprimitive
Mathlib.Meta.NormNum.isNat_le_true
Mathlib.Meta.NormNum.isNat_ofNat
of_surjective
Function.Bijective.surjective
SubMulAction.ofFixingSubgroup_of_eq_bijective
Subgroup.instIsScalarTowerSubtypeMem
SubMulAction.isScalarTower'
SubMulAction.ofFixingSubgroup_insert_map_bijective
Set.ncard_image_of_injective
Subtype.val_injective
Set.ncard_insert_of_notMem
Finite.Set.finite_image
SubMulAction.nat_card_ofStabilizer_add_one_eq
Nat.strong_induction_on
Nat.finite_of_card_ne_zero
ne_zero_of_lt
Set.ncard_univ
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono
AddLeftCancelSemigroup.toIsLeftCancelAdd
IsOrderedAddMonoid.toAddLeftMono
Nat.instIsOrderedAddMonoid
contravariant_lt_of_covariant_le
Nat.instZeroLEOneClass
IsRightCancelAdd.addRightStrictMono_of_addRightMono
AddRightCancelSemigroup.toIsRightCancelAdd
covariant_swap_add_of_covariant_add
contravariant_swap_add_of_contravariant_add
Nat.instNoMaxOrder
SubMulAction.ofStabilizer.isMultiplyPretransitive
MulAction.is_one_pretransitive_iff
MulAction.IsPretransitive.of_surjective_map
SubMulAction.ofFixingSubgroup_of_singleton_bijective
le_rfl
Set.one_lt_ncard
exists_mem_smul_and_notMem_smul
Set.Finite.inter_of_left
Set.ncard_ne_zero_of_mem
Set.ncard_lt_ncard
Set.inter_subset_left
Set.inter_subset_right
lt_trans
SubMulAction.IsPretransitive.isPretransitive_ofFixingSubgroup_inter
Set.union_ne_univ_of_ncard_add_ncard_lt
Set.ncard_smul_set
two_mul
SubMulAction.IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Set.one_lt_encard_iff_nontrivial
Set.Finite.cast_ncard_eq
Nat.one_lt_cast
IsOrderedRing.toIsOrderedAddMonoid
IsOrderedRing.toZeroLEOneClass
Set.nonempty_of_mem
Set.smul_set_compl
Finite.Set.finite_inter_of_left
Set.nonempty_inter_of_le_ncard_add_ncard
Set.eq_of_subset_of_ncard_le
subset_trans
Set.instIsTransSubset
le_refl
Set.mem_univ
ENat
Preorder.toLT
OmegaCompletePartialOrder.toPartialOrder
CompleteLattice.instOmegaCompletePartialOrder
CompletelyDistribLattice.toCompleteLattice
CompleteLinearOrder.toCompletelyDistribLattice
instCompleteLinearOrderENat
instOfNatAtLeastTwo
ENat.instNatCast
ENat.card
Subgroup.normalClosure
MulAction.stabilizer
one_le_two
le_of_lt
ENat.one_lt_card_iff_nontrivial
Mathlib.Meta.NormNum.isNat_lt_true
Nat.cast_one
Mathlib.Meta.NormNum.instAtLeastTwo
MulAction.isCoatom_stabilizer_iff_preprimitive
MulAction.isPreprimitive_of_is_two_pretransitive
Subgroup.le_normalClosure
lt_of_add_lt_add_right
SubMulAction.ENat_card_ofStabilizer_add_one_eq
nontrivial_iff
MulAction.exists_smul_eq
SubMulAction.instSMulMemClass
SetLike.val_smul
inv_smul_eq_iff
Subgroup.Normal.conj_mem
Subgroup.normalClosure_normal
---
← Back to Index