Alternating

📁 Source: Mathlib/GroupTheory/SpecificGroups/Alternating.lean

Statistics

Metric	Count
Definitions altCongrHom, alternatingGroup, instFintype, instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton	4
Theorems alternating_normalClosure, mem_alternatingGroup, alternatingGroup_le_of_index_le_two, closure_cycleType_eq_2_2_eq_alternatingGroup, closure_three_cycles_eq_alternating, eq_alternatingGroup_of_index_eq_two, finRotate_bit1_mem_alternatingGroup, isThreeCycle_sq_of_three_mem_cycleType_five, mem_alternatingGroup, mul_mem_alternatingGroup_of_isSwap, prod_list_swap_mem_alternatingGroup_iff_even_length, altCongrHom_apply_coe, center_eq_bot, eq_bot_of_card_le_two, index_eq_one, index_eq_two, instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup, isConj_of, isConj_swap_mul_swap_of_cycleType_two, isSimpleGroup_five, isThreeCycle_isConj, nontrivial_of_three_le_card, normal, normalClosure_finRotate_five, normalClosure_swap_mul_swap_five, alternatingGroup_eq_sign_ker, card_alternatingGroup, instCharacteristicPermAlternatingGroup, nat_card_alternatingGroup, two_mul_card_alternatingGroup, two_mul_nat_card_alternatingGroup	31
Total	35

Equiv

Definitions

Name	Category	Theorems
altCongrHom 📖	CompOp	1 math math: altCongrHom_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
altCongrHom_apply_coe 📖	mathematical	—	Perm Subgroup Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup DFunLike.coe MulEquiv Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike altCongrHom Equiv instEquivLike permCongr	—	—

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingGroup_le_of_index_le_two 📖	mathematical	Subgroup.index Equiv.Perm permGroup	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder alternatingGroup	—	Subgroup.index_ne_zero_of_finite Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_of_finite Equiv.finite_left Finite.of_fintype LE.le.eq_or_lt' le_top Subgroup.index_eq_one eq_alternatingGroup_of_index_eq_two LE.le.antisymm le_refl
closure_cycleType_eq_2_2_eq_alternatingGroup 📖	mathematical	Nat.card	Subgroup.closure Equiv.Perm permGroup setOf Multiset cycleType Multiset.instInsert Multiset.instSingleton alternatingGroup	—	le_antisymm Subgroup.closure_le sign_of_cycleType Multiset.sum_cons Multiset.sum_singleton Multiset.card_cons Multiset.card_singleton closure_three_cycles_eq_alternating IsCycle.nonempty_support IsThreeCycle.isCycle IsThreeCycle.support_eq_iff_mem_support IsThreeCycle.nodup_iff_mem_support Finset.one_lt_card_iff mul_assoc Equiv.swap_mul_self_mul IsThreeCycle.eq_swap_mul_swap_iff_mem_support MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.subset_closure cycleType_swap_mul_swap_of_nodup
closure_three_cycles_eq_alternating 📖	mathematical	—	Subgroup.closure Equiv.Perm permGroup setOf IsThreeCycle alternatingGroup	—	Subgroup.closure_eq_of_le mem_alternatingGroup IsThreeCycle.sign SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass List.exists_of_length_succ mul_assoc MulMemClass.mul_mem SubmonoidClass.toMulMemClass IsSwap.mul_mem_closure_three_cycles prod_list_swap_mem_alternatingGroup_iff_even_length Nat.instAtLeastTwoHAddOfNat two_mul
eq_alternatingGroup_of_index_eq_two 📖	mathematical	Subgroup.index Equiv.Perm permGroup	alternatingGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Equiv.equiv_subsingleton_dom eq_top_iff closure_isSwap Finite.of_fintype Subgroup.closure_le Mathlib.Tactic.Push.not_and_eq Subgroup.index_top Subgroup.ext swap_induction_on Subgroup.one_mem map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass Subgroup.mul_mem_iff_of_index_two alternatingGroup.index_eq_two Mathlib.Tactic.Contrapose.contrapose₄ isConj_iff isConj_swap Subgroup.Normal.conj_mem Subgroup.normal_of_index_eq_two sign_swap
finRotate_bit1_mem_alternatingGroup 📖	mathematical	—	Equiv.Perm Subgroup permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype finRotate	—	mem_alternatingGroup sign_finRotate pow_mul pow_two Int.units_mul_self one_pow
isThreeCycle_sq_of_three_mem_cycleType_five 📖	mathematical	Multiset Multiset.instMembership cycleType Fin.fintype	IsThreeCycle Equiv.Perm instMul	—	mem_cycleType_iff IsThreeCycle.congr_simp mul_assoc Commute.eq Disjoint.commute lcm_cycleType Multiset.lcm_dvd le_antisymm two_le_of_mem_cycleType le_trans le_card_support_of_mem_cycleType le_of_add_le_add_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Disjoint.card_support_mul Finset.card_le_univ dvd_refl pow_two orderOf_dvd_iff_pow_eq_one one_mul IsThreeCycle.isThreeCycle_sq card_support_eq_three_iff
mem_alternatingGroup 📖	mathematical	—	Equiv.Perm Subgroup permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup DFunLike.coe MonoidHom Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instMulOneClass MonoidHom.instFunLike sign Units.instOne	—	MonoidHom.mem_ker
mul_mem_alternatingGroup_of_isSwap 📖	mathematical	IsSwap	Equiv.Perm Subgroup permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup instMul	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass IsSwap.sign_eq mul_neg mul_one neg_neg
prod_list_swap_mem_alternatingGroup_iff_even_length 📖	mathematical	IsSwap	Equiv.Perm Subgroup permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup instMul instOne Even	—	mem_alternatingGroup sign_prod_list_swap neg_one_pow_eq_one_iff_even

Equiv.Perm.IsThreeCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternating_normalClosure 📖	mathematical	Fintype.card Equiv.Perm.IsThreeCycle	Subgroup.normalClosure Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Subgroup.toGroup Set Set.instSingletonSet mem_alternatingGroup Top.top Subgroup.instTop	—	mem_alternatingGroup eq_top_iff Subtype.coe_injective Subgroup.map_injective le_antisymm Subgroup.map_mono le_top MonoidHom.range_eq_map Subgroup.range_subtype Subgroup.normalClosure.eq_1 MonoidHom.map_closure LE.le.trans le_of_eq Equiv.Perm.closure_three_cycles_eq_alternating Subgroup.closure_mono isConj_iff Equiv.Perm.isConj_iff_cycleType_eq Group.mem_conjugatesOfSet_iff Set.mem_singleton alternatingGroup.isThreeCycle_isConj
mem_alternatingGroup 📖	mathematical	Equiv.Perm.IsThreeCycle	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup	—	Equiv.Perm.mem_alternatingGroup sign

(root)

Definitions

Name	Category	Theorems
alternatingGroup 📖	CompOp	64 math math: alternatingGroup.eq_bot_of_card_le_two, alternatingGroup.commutator_perm_eq, alternatingGroup.isPreprimitive_of_three_le_card, Equiv.Perm.eq_alternatingGroup_of_index_eq_two, alternatingGroup.card_two_sylow_of_card_eq_four, alternatingGroup.kleinFour_card_of_card_eq_four, AlternatingGroup.isPreprimitive_of_three_le_card, Equiv.altCongrHom_apply_coe, Equiv.Perm.alternatingGroup_le_of_index_le_two, alternatingGroup.normalClosure_swap_mul_swap_five, alternatingGroup.subsingleton_two_sylow, Equiv.Perm.mul_mem_alternatingGroup_of_isSwap, alternatingGroup.isCoatom_stabilizer_singleton, alternatingGroup.characteristic_kleinFour, Set.powersetCard.isPretransitive_alternatingGroup, alternatingGroup.kleinFour_isKleinFour, AlternatingGroup.card_of_cycleType_singleton, alternatingGroup.normalClosure_finRotate_five, alternatingGroup.kleinFour_eq_commutator, alternatingGroup.center_eq_bot, alternatingGroup.stabilizer.surjective_toPerm, alternatingGroup.coe_kleinFour_of_card_eq_four, Equiv.Perm.mem_alternatingGroup, instCharacteristicPermAlternatingGroup, AlternatingGroup.card_of_cycleType, Equiv.Perm.finRotate_bit1_mem_alternatingGroup, Equiv.Perm.centralizer_le_alternating_iff, alternatingGroup.index_eq_one, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four, alternatingGroup.nontrivial_of_three_le_card, Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem, AlternatingGroup.isMultiplyPretransitive, alternatingGroup.exists_mem_stabilizer_smul_eq, alternatingGroup.coe_two_sylow_of_card_eq_four, two_mul_card_alternatingGroup, commutator_alternatingGroup_eq_top, AlternatingGroup.isPretransitive_of_three_le_card, card_alternatingGroup, alternatingGroup.stabilizer_isPreprimitive, Equiv.Perm.prod_list_swap_mem_alternatingGroup_iff_even_length, two_mul_nat_card_alternatingGroup, Equiv.Perm.IsThreeCycle.alternating_normalClosure, alternatingGroup.normal, alternatingGroup.normal_kleinFour, alternatingGroup.isSimpleGroup_five, alternatingGroup.isCoatom_stabilizer, alternatingGroup.exponent_kleinFour_of_card_eq_four, Set.powersetCard.isPreprimitive_alternatingGroup, alternatingGroup.instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup, alternatingGroup.commutator_perm_le, alternatingGroup.isPretransitive_of_three_le_card, IsMultiplyPretransitive.alternatingGroup_le, alternatingGroup.isMultiplyPretransitive, alternatingGroup.card_of_card_eq_four, AlternatingGroup.map_subtype_of_cycleType, nat_card_alternatingGroup, Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup, alternatingGroup_eq_sign_ker, alternatingGroup.index_eq_two, commutator_alternatingGroup_eq_self, Equiv.Perm.IsThreeCycle.mem_alternatingGroup, AlternatingGroup.card_of_cycleType_mul_eq, Equiv.Perm.closure_three_cycles_eq_alternating, alternatingGroup.isCoatom_stabilizer_of_ncard_lt_ncard_compl
instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingGroup_eq_sign_ker 📖	mathematical	—	alternatingGroup MonoidHom.ker Equiv.Perm Equiv.Perm.permGroup Units Int.instMonoid Units.instMulOneClass Equiv.Perm.sign	—	—
card_alternatingGroup 📖	mathematical	—	Fintype.card Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup alternatingGroup.instFintype Nat.factorial	—	two_ne_zero two_mul_card_alternatingGroup Fintype.card_perm
instCharacteristicPermAlternatingGroup 📖	mathematical	—	Subgroup.Characteristic Equiv.Perm Equiv.Perm.permGroup alternatingGroup	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass Unique.instSubsingleton Equiv.equiv_subsingleton_dom Equiv.Perm.eq_alternatingGroup_of_index_eq_two Subgroup.index_comap_of_surjective Equiv.surjective alternatingGroup.index_eq_two
nat_card_alternatingGroup 📖	mathematical	—	Nat.card Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Nat.factorial	—	Nat.card_eq_fintype_card card_alternatingGroup
two_mul_card_alternatingGroup 📖	mathematical	—	Fintype.card Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup alternatingGroup.instFintype Equiv.instFintype	—	two_mul_nat_card_alternatingGroup
two_mul_nat_card_alternatingGroup 📖	mathematical	—	Nat.card Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup	—	alternatingGroup.index_eq_two Subgroup.index_mul_card

alternatingGroup

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	6 math math: AlternatingGroup.card_of_cycleType_singleton, AlternatingGroup.card_of_cycleType, two_mul_card_alternatingGroup, card_alternatingGroup, AlternatingGroup.map_subtype_of_cycleType, AlternatingGroup.card_of_cycleType_mul_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_eq_bot 📖	mathematical	Nat.card	Subgroup.center Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Subgroup.toGroup Bot.bot Subgroup.instBot	—	eq_bot_iff Equiv.Perm.mem_support Finset.card_add_card_compl Nat.card_eq_fintype_card Finset.card_pair Finset.one_lt_card_iff Equiv.Perm.coe_mul Equiv.swap_apply_of_ne_of_ne Finset.compl_insert Equiv.swap_apply_left Equiv.Perm.sign_mul Equiv.Perm.sign_swap' mul_neg mul_one neg_neg Subgroup.mk_smul Subgroup.mem_center_iff
eq_bot_of_card_le_two 📖	mathematical	Fintype.card	alternatingGroup Bot.bot Subgroup Equiv.Perm Equiv.Perm.permGroup Subgroup.instBot	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Equiv.equiv_subsingleton_dom LE.le.antisymm Fintype.one_lt_card Subgroup.eq_bot_iff_card Nat.instCharZero Nat.instAtLeastTwoHAddOfNat Nat.card_eq_fintype_card two_mul_card_alternatingGroup mul_one Fintype.card_perm Nat.factorial_two
index_eq_one 📖	mathematical	—	Subgroup.index Equiv.Perm Equiv.Perm.permGroup alternatingGroup	—	Subgroup.index_eq_one Unique.instSubsingleton Equiv.equiv_subsingleton_dom
index_eq_two 📖	mathematical	—	Subgroup.index Equiv.Perm Equiv.Perm.permGroup alternatingGroup	—	eq_1 Subgroup.index_ker MonoidHom.range_eq_top Equiv.Perm.sign_surjective Nat.card_eq_fintype_card Fintype.card_subtype_true
instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup 📖	mathematical	—	Nontrivial Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype	—	nontrivial_of_three_le_card Fintype.card_fin le_add_left Nat.instCanonicallyOrderedAdd le_refl
isConj_of 📖	mathematical	IsConj Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Subgroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Finset.card Equiv.Perm.support Fintype.card	Subgroup.toGroup	—	isConj_iff Int.units_eq_one_or Equiv.Perm.mem_alternatingGroup Subtype.val_injective Finset.card_compl le_tsub_iff_left CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Finset.card_le_univ Finset.one_lt_card map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass Equiv.Perm.sign_swap Int.units_mul_self Equiv.Perm.disjoint_iff_disjoint_support Equiv.Perm.support_swap Finset.disjoint_insert_left Finset.disjoint_singleton_left Finset.mem_compl mul_assoc Commute.eq Equiv.Perm.Disjoint.commute mul_inv_rev Equiv.swap_mul_self_mul
isConj_swap_mul_swap_of_cycleType_two 📖	mathematical	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype	IsConj DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.instMul Equiv.swap	—	Finset.card_le_univ le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.instIsStrictOrderedRing le_trans smul_eq_mul Multiset.sum_replicate Multiset.eq_replicate_card Equiv.Perm.sum_cycleType Fintype.card_fin Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instAtLeastTwoHAddOfNat Nat.instNontrivial Equiv.Perm.isConj_iff_cycleType_eq le_antisymm Mathlib.Tactic.IntervalCases.of_le_right Mathlib.Meta.NormNum.IsNat.to_raw_eq neg_one_pow_eq_one_iff_even one_mul Int.units_pow_two pow_mul pow_add Multiset.card_replicate Equiv.Perm.sign_of_cycleType Equiv.Perm.mem_alternatingGroup Equiv.Perm.Disjoint.cycleType_mul Equiv.Perm.disjoint_iff_disjoint_support Equiv.Perm.support_swap Equiv.Perm.IsCycle.cycleType Equiv.Perm.isCycle_swap Equiv.Perm.card_support_swap Equiv.Perm.card_cycleType_eq_zero
isSimpleGroup_five 📖	mathematical	—	IsSimpleGroup Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype Subgroup.toGroup	—	instNontrivialSubtypePermFinHAddNatOfNatMemSubgroup Mathlib.Tactic.Push.not_forall_eq Subgroup.eq_bot_iff_forall eq_top_iff le_trans ge_of_eq IsConj.normalClosure_eq_top_of normal Equiv.Perm.mem_alternatingGroup isConj_swap_mul_swap_of_cycleType_two normalClosure_swap_mul_swap_five lt_of_le_of_ne Equiv.Perm.two_le_of_mem_cycleType Multiset.exists_cons_of_mem Equiv.Perm.sum_cycleType Multiset.sum_cons le_add_right Nat.instCanonicallyOrderedAdd le_rfl Finset.card_le_univ Equiv.Perm.finRotate_bit1_mem_alternatingGroup Equiv.Perm.isConj_iff_cycleType_eq Equiv.Perm.cycleType_of_card_le_mem_cycleType_add_two cycleType_finRotate normalClosure_finRotate_five le_antisymm Mathlib.Tactic.IntervalCases.of_le_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_ofNat Multiset.sum_singleton Multiset.card_singleton Odd.neg_one_pow Int.instCharZero Equiv.Perm.sign_of_cycleType Equiv.Perm.IsThreeCycle.mem_alternatingGroup Equiv.Perm.isThreeCycle_sq_of_three_mem_cycleType_five Equiv.Perm.IsThreeCycle.alternating_normalClosure Fintype.card_fin le_refl Subgroup.normalClosure_le_normal Subgroup.normalClosure_normal Set.singleton_subset_iff SetLike.mem_coe Subgroup.subset_normalClosure Set.mem_singleton MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Mathlib.Tactic.IntervalCases.of_lt_left or_not
isThreeCycle_isConj 📖	mathematical	Fintype.card Equiv.Perm.IsThreeCycle Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup	IsConj DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	isConj_of Equiv.Perm.isConj_iff_cycleType_eq Equiv.Perm.IsThreeCycle.card_support
nontrivial_of_three_le_card 📖	mathematical	Fintype.card	Nontrivial Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup	—	Fintype.one_lt_card_iff_nontrivial lt_of_mul_lt_mul_left PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono two_mul_card_alternatingGroup lt_trans Fintype.card_perm le_trans Nat.self_le_factorial le_of_lt Nat.Prime.pos Nat.prime_two
normal 📖	mathematical	—	Subgroup.Normal Equiv.Perm Equiv.Perm.permGroup alternatingGroup	—	MonoidHom.normal_ker
normalClosure_finRotate_five 📖	mathematical	—	Subgroup.normalClosure Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype Subgroup.toGroup Set Set.instSingletonSet finRotate Equiv.Perm.finRotate_bit1_mem_alternatingGroup Top.top Subgroup.instTop	—	Equiv.Perm.finRotate_bit1_mem_alternatingGroup eq_top_iff card_support_eq_three_iff Equiv.Perm.IsThreeCycle.mem_alternatingGroup Equiv.Perm.IsThreeCycle.alternating_normalClosure Fintype.card_fin le_refl Subgroup.normalClosure_le_normal Subgroup.normalClosure_normal Set.singleton_subset_iff SetLike.mem_coe Subgroup.subset_normalClosure Set.mem_singleton MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Fin.isThreeCycle_cycleRange_two Subgroup.Normal.conj_mem InvMemClass.inv_mem SubgroupClass.toInvMemClass
normalClosure_swap_mul_swap_five 📖	mathematical	—	Subgroup.normalClosure Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Fin.fintype Subgroup.toGroup Set Set.instSingletonSet Equiv.Perm.instMul Equiv.swap Units Int.instMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign Units.instOne Equiv.Perm.mem_alternatingGroup Top.top Subgroup.instTop	—	Equiv.Perm.mem_alternatingGroup Equiv.Perm.finRotate_bit1_mem_alternatingGroup eq_top_iff normalClosure_finRotate_five Subgroup.normalClosure_le_normal Subgroup.normalClosure_normal Set.singleton_subset_iff SetLike.mem_coe Subgroup.subset_normalClosure Set.mem_singleton MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.Normal.conj_mem InvMemClass.inv_mem SubgroupClass.toInvMemClass

---

← Back to Index