Alternating

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

Statistics

Metric	Count
Definitions altCongrHom, alternatingGroup, instFintype, ofSubtype, instUniqueSubtypePermMemSubgroupAlternatingGroupOfSubsingleton	5
Theorems alternating_normalClosure, mem_alternatingGroup, alternatingGroup_le_of_index_le_two, closure_cycleType_eq_2_2_eq_alternatingGroup, closure_cycleType_eq_two_two_eq_alternatingGroup, closure_three_cycles_eq_alternating, cycleType_eq_two_two_subset_alternatingGroup, eq_alternatingGroup_of_index_eq_two, finRotate_bit1_mem_alternatingGroup, isThreeCycle_sq_of_three_mem_cycleType_five, isThreeCycle_subset_alternatingGroup, mem_alternatingGroup, mul_mem_alternatingGroup_of_isSwap, prod_list_swap_mem_alternatingGroup_iff_even_length, altCongrHom_apply_coe, center_eq_bot, closure_cycleType_eq_two_two_eq_top, closure_isThreeCycles_eq_top, conj_smul_range_ofSubtype, 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, map_ofSubtype, mem_range_ofSubtype_iff, nontrivial_of_three_le_card, normal, normalClosure_finRotate_five, normalClosure_swap_mul_swap_five, ofSubtype_comp_subtype, range_ofSubtype, alternatingGroup_eq_sign_ker, card_alternatingGroup, instCharacteristicPermAlternatingGroup, nat_card_alternatingGroup, two_mul_card_alternatingGroup, two_mul_nat_card_alternatingGroup	41
Total	46

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 Equiv.Perm permGroup 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	—	closure_cycleType_eq_two_two_eq_alternatingGroup
closure_cycleType_eq_two_two_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 IsThreeCycle.mem_alternatingGroup SubmonoidClass.toOneMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass List.exists_of_length_succ mul_assoc MulMemClass.mul_mem SubmonoidClass.toMulMemClass prod_list_swap_mem_alternatingGroup_iff_even_length Nat.instAtLeastTwoHAddOfNat two_mul
cycleType_eq_two_two_subset_alternatingGroup 📖	mathematical	—	Set Equiv.Perm Set.instHasSubset setOf Multiset cycleType Multiset.instInsert Multiset.instSingleton SetLike.coe Subgroup permGroup Subgroup.instSetLike alternatingGroup	—	sign_of_cycleType Set.mem_setOf_eq Multiset.sum_cons Multiset.sum_singleton Multiset.card_cons Multiset.card_singleton
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 Fin.fintype 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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
isThreeCycle_subset_alternatingGroup 📖	mathematical	—	Set Equiv.Perm Set.instHasSubset setOf IsThreeCycle SetLike.coe Subgroup permGroup Subgroup.instSetLike alternatingGroup	—	IsThreeCycle.mem_alternatingGroup
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 Subgroup.map_subtype_le_map_subtype 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	81 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, Equiv.Perm.isThreeCycle_subset_alternatingGroup, alternatingGroup.card_two_sylow_of_card_eq_four, alternatingGroup.kleinFour_card_of_card_eq_four, Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup, 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, Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup, alternatingGroup.closure_isThreeCycles_eq_top, alternatingGroup.characteristic_kleinFour, Set.powersetCard.isPretransitive_alternatingGroup, alternatingGroup.kleinFour_isKleinFour, AlternatingGroup.card_of_cycleType_singleton, alternatingGroup.mem_range_ofSubtype_iff, alternatingGroup.normalClosure_finRotate_five, alternatingGroup.kleinFour_eq_commutator, alternatingGroup.center_eq_bot, alternatingGroup.stabilizer.surjective_toPerm, alternatingGroup.closure_cycleType_eq_two_two_eq_top, alternatingGroup.coe_kleinFour_of_card_eq_four, alternatingGroup.map_ofSubtype, Equiv.Perm.mem_alternatingGroup, alternatingGroup.isConj_of, instCharacteristicPermAlternatingGroup, AlternatingGroup.card_of_cycleType, Equiv.Perm.finRotate_bit1_mem_alternatingGroup, Equiv.Perm.centralizer_le_alternating_iff, alternatingGroup.index_eq_one, alternatingGroup.subgroup_eq_top_of_isPreprimitive, Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroup, 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.range_ofSubtype, 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, Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup, IsMultiplyPretransitive.alternatingGroup_le, alternatingGroup.isMultiplyPretransitive, Equiv.Perm.alternatingGroup_le_of_isPreprimitive, alternatingGroup.card_of_card_eq_four, alternatingGroup.isThreeCycle_isConj, 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, alternatingGroup.stabilizer_subgroup_isPreprimitive, Equiv.Perm.IsThreeCycle.mem_alternatingGroup, AlternatingGroup.card_of_cycleType_mul_eq, Equiv.Perm.closure_three_cycles_eq_alternating, alternatingGroup.conj_smul_range_ofSubtype, alternatingGroup.ofSubtype_comp_subtype, 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
ofSubtype 📖	CompOp	4 math math: mem_range_ofSubtype_iff, range_ofSubtype, conj_smul_range_ofSubtype, ofSubtype_comp_subtype

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
closure_cycleType_eq_two_two_eq_top 📖	mathematical	Nat.card	Subgroup.closure Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Subgroup.toGroup setOf Multiset Equiv.Perm.cycleType Multiset.instInsert Multiset.instSingleton Top.top Subgroup.instTop	—	MonoidHom.map_closure Subtype.coe_image_of_subset Equiv.Perm.cycleType_eq_two_two_subset_alternatingGroup Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup Set.image_congr Subgroup.ext
closure_isThreeCycles_eq_top 📖	mathematical	—	Subgroup.closure Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Subgroup.toGroup setOf Equiv.Perm.IsThreeCycle Top.top Subgroup.instTop	—	MonoidHom.map_closure Subtype.coe_image_of_subset Equiv.Perm.isThreeCycle_subset_alternatingGroup Set.image_congr Equiv.Perm.closure_three_cycles_eq_alternating Subgroup.ext
conj_smul_range_ofSubtype 📖	mathematical	—	MulAut Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup SemigroupAction.toSMul Monoid.toSemigroup MulAut.instGroup MulAction.toSemigroupAction Subgroup.pointwiseMulAction MulAut.applyMulDistribMulAction DFunLike.coe MonoidHom MonoidHom.instFunLike MulAut.conj MonoidHom.range Finset Finset.instSetLike Finset.Subtype.fintype ofSubtype Finset.smulFinset Subgroup.instMulAction Equiv.Perm.applyMulAction	—	Subgroup.ext MonoidHom.instMonoidHomClass ConjAct.coe_smul Equiv.Perm.support_conj_eq_smul_support
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 covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd
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	IsConj Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup DivInvMonoid.toMonoid Group.toDivInvMonoid 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid 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 Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup 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.instNoMaxOrder Nat.instCanonicallyOrderedAdd 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 Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	—	isConj_of Equiv.Perm.isConj_iff_cycleType_eq Equiv.Perm.IsThreeCycle.card_support
map_ofSubtype 📖	mathematical	—	Subgroup.map Equiv.Perm Finset SetLike.instMembership Finset.instSetLike Equiv.Perm.permGroup Equiv.Perm.ofSubtype Finset.decidableMem alternatingGroup Finset.Subtype.fintype Subgroup Subgroup.instMin MonoidHom.range	—	Subgroup.ext Subgroup.mem_map Subgroup.mem_inf MonoidHom.mem_range
mem_range_ofSubtype_iff 📖	mathematical	—	Equiv.Perm Subgroup Equiv.Perm.permGroup SetLike.instMembership Subgroup.instSetLike alternatingGroup Subgroup.toGroup MonoidHom.range Finset Finset.instSetLike Finset.Subtype.fintype ofSubtype Finset.instHasSubset Equiv.Perm.support	—	range_ofSubtype Subgroup.mem_subgroupOf Equiv.Perm.mem_range_ofSubtype_iff instIsConcreteLE
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
ofSubtype_comp_subtype 📖	mathematical	—	MonoidHom.comp Equiv.Perm Finset SetLike.instMembership Finset.instSetLike Subgroup Equiv.Perm.permGroup Subgroup.instSetLike alternatingGroup Finset.Subtype.fintype MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.subtype ofSubtype Equiv.Perm.ofSubtype Finset.decidableMem	—	—
range_ofSubtype 📖	mathematical	—	MonoidHom.range Equiv.Perm Finset SetLike.instMembership Finset.instSetLike Subgroup Equiv.Perm.permGroup Subgroup.instSetLike alternatingGroup Finset.Subtype.fintype Subgroup.toGroup ofSubtype Subgroup.subgroupOf Equiv.Perm.ofSubtype Finset.decidableMem	—	MonoidHom.range_comp ofSubtype_comp_subtype Subgroup.range_subtype Subgroup.subgroupOf_map_subtype map_ofSubtype

---

← Back to Index