Sylow

📁 Source: Mathlib/GroupTheory/Sylow.lean

Statistics

Metric	Count
Definitions toSylow, Sylow, comapOfInjective, comapOfKerIsPGroup, directProductOfNormal, equiv, equivQuotientNormalizer, equivSMul, fixedPointsMulLeftCosetsEquivQuotient, inhabited, instCoeOutSubgroup, instPartialOrder, instSetLike, mapSurjective, mulAction, ofCard, pointwiseMulAction, subtype, toSubgroup, unique_of_normal	20
Theorems exists_le_sylow, inf_normalizer_sylow, mem_toSylow, sylow_mem_fixedPoints_iff, toSylow_coe, card_preimage_mk, sylow_mem_fixedPoints_iff, card_coprime_index, card_dvd_index, card_eq_card_quotient_normalizer, card_eq_index_normalizer, card_eq_multiplicity, card_normalizer_modEq_card, card_quotient_normalizer_modEq_card_quotient, characteristic_of_normal, characteristic_of_subsingleton, coe_comapOfInjective, coe_comapOfKerIsPGroup, coe_mapSurjective, coe_ofCard, coe_smul, coe_subgroup_smul, coe_subtype, conj_eq_normalizer_conj_of_mem, conj_eq_normalizer_conj_of_mem_centralizer, dvd_card_of_dvd_card, exists_comap_eq_of_injective, exists_comap_eq_of_ker_isPGroup, exists_comap_subtype_eq, exists_subgroup_card_pow_prime, exists_subgroup_card_pow_prime_le, exists_subgroup_card_pow_prime_of_le_card, exists_subgroup_card_pow_succ, exists_subgroup_le_card_le, exists_subgroup_le_card_pow_prime_of_le_card, ext, ext_iff, finite_of_finiteIndex, finite_of_injective, finite_of_ker_is_pGroup, instFiniteQuotientSubgroupNormalizer, instFiniteSubtypeMemSubgroup, instSubgroupClass, isPGroup', isPretransitive_of_finite, is_maximal', mapSurjective_surjective, mem_fixedPoints_mul_left_cosets_iff_mem_normalizer, ne_bot_of_dvd_card, nonempty, normal_of_all_max_subgroups_normal, normal_of_normalizerCondition, normal_of_normalizer_normal, normal_of_subsingleton, normalizer_normalizer, normalizer_sup_eq_top, normalizer_sup_eq_top', not_dvd_index, not_dvd_index', orbit_eq_top, pointwise_smul_def, pow_dvd_card_of_pow_dvd_card, prime_dvd_card_quotient_normalizer, prime_pow_dvd_card_normalizer, smul_def, smul_eq_iff_mem_normalizer, smul_eq_of_normal, smul_le, smul_subtype, stabilizer_eq_normalizer, subtype_injective, card_sylow_modEq_one, not_dvd_card_sylow	73
Total	93

IsPGroup

Definitions

Name	Category	Theorems
toSylow 📖	CompOp	2 math math: toSylow_coe, mem_toSylow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_le_sylow 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	Sylow Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Sylow.toSubgroup	—	zorn_le_nonempty₀ IsChain.total instReflLe Subgroup.mul_mem Subgroup.one_mem Subgroup.inv_mem Subgroup.coe_pow Maximal.prop Maximal.eq_of_ge
inf_normalizer_sylow 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	Subgroup Subgroup.instMin Subgroup.normalizer SetLike.coe Subgroup.instSetLike Sylow.toSubgroup	—	le_antisymm le_inf inf_le_left sup_eq_right Sylow.is_maximal' to_sup_of_normal_right' to_inf_left Sylow.isPGroup' inf_le_right le_sup_right inf_le_inf_left Subgroup.le_normalizer
mem_toSylow 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.index	Sylow SetLike.instMembership Sylow.instSetLike toSylow Subgroup Subgroup.instSetLike	—	—
sylow_mem_fixedPoints_iff 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	Sylow Set Set.instMembership MulAction.fixedPoints Subgroup SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Subgroup.instMulAction Sylow.mulAction Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Sylow.toSubgroup	—	Subgroup.sylow_mem_fixedPoints_iff inf_eq_left inf_normalizer_sylow
toSylow_coe 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.index	Sylow.toSubgroup toSylow	—	—

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_preimage_mk 📖	mathematical	—	Nat.card Set.Elem Set.preimage HasQuotient.Quotient Subgroup instHasQuotientSubgroup SetLike.instMembership Subgroup.instSetLike	—	Nat.card_prod Nat.card_congr

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sylow_mem_fixedPoints_iff 📖	mathematical	—	Sylow Set Set.instMembership MulAction.fixedPoints Subgroup SetLike.instMembership instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup instMulAction Sylow.mulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder normalizer SetLike.coe Sylow.toSubgroup	—	instIsConcreteLE

Sylow

Definitions

Name	Category	Theorems
comapOfInjective 📖	CompOp	1 math math: coe_comapOfInjective
comapOfKerIsPGroup 📖	CompOp	1 math math: coe_comapOfKerIsPGroup
directProductOfNormal 📖	CompOp	—
equiv 📖	CompOp	—
equivQuotientNormalizer 📖	CompOp	—
equivSMul 📖	CompOp	—
fixedPointsMulLeftCosetsEquivQuotient 📖	CompOp	—
inhabited 📖	CompOp	—
instCoeOutSubgroup 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instSetLike 📖	CompOp	8 math math: coe_smul, MonoidHom.transferSylow_restrict_eq_pow, normalizer_le_centralizer_or_le_commutator, alternatingGroup.coe_two_sylow_of_card_eq_four, IsPGroup.mem_toSylow, instSubgroupClass, Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf, IsCyclic.normalizer_le_centralizer
mapSurjective 📖	CompOp	2 math math: mapSurjective_surjective, coe_mapSurjective
mulAction 📖	CompOp	12 math math: IsPGroup.sylow_mem_fixedPoints_iff, coe_smul, smul_eq_iff_mem_normalizer, stabilizer_eq_normalizer, orbit_eq_top, Subgroup.sylow_mem_fixedPoints_iff, smul_eq_of_normal, coe_subgroup_smul, smul_subtype, isPretransitive_of_finite, smul_le, smul_def
ofCard 📖	CompOp	1 math math: coe_ofCard
pointwiseMulAction 📖	CompOp	2 math math: pointwise_smul_def, smul_def
subtype 📖	CompOp	2 math math: coe_subtype, smul_subtype
toSubgroup 📖	CompOp	63 math math: coe_comapOfKerIsPGroup, isPGroup', not_dvd_index', MonoidHom.ker_transferSylow_disjoint, IsCyclic.isComplement', MonoidHom.transferSylow_eq_pow, pointwise_smul_def, IsPGroup.sylow_mem_fixedPoints_iff, normalizer_normalizer, Subgroup.focalSubgroupOf.pow_index_surjective, Subgroup.transferFocal_surjective, alternatingGroup.card_two_sylow_of_card_eq_four, MonoidHom.ker_transferSylow_isComplement', normal_of_normalizerCondition, card_dvd_index, coe_ofCard, normalizer_sup_eq_top', smul_eq_iff_mem_normalizer, normal_of_all_max_subgroups_normal, not_dvd_index, ext_iff, MonoidHom.not_dvd_card_ker_transferSylow, MonoidHom.transferSylow_restrict_eq_pow, stabilizer_eq_normalizer, normal_of_subsingleton, characteristic_of_subsingleton, instFiniteQuotientSubgroupNormalizer, Subgroup.sylow_mem_fixedPoints_iff, exists_comap_eq_of_injective, conj_eq_normalizer_conj_of_mem, characteristic_of_normal, normalizer_le_centralizer_or_le_commutator, le_center_or_le_commutator, is_maximal', commutator_eq_bot_or_commutator_eq_self, IsPGroup.exists_le_sylow, isNilpotent_of_finite_tfae, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four, IsPGroup.toSylow_coe, card_eq_multiplicity, coe_comapOfInjective, Subgroup.commutator_inf_eq_focalSubgroup, coe_subgroup_smul, coe_subtype, normalizer_sup_eq_top, dvd_card_of_dvd_card, exists_comap_subtype_eq, normal_of_normalizer_normal, Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf, Subgroup.ker_transferFocal_inf_eq_focalSubgroup, IsPGroup.inf_normalizer_sylow, coe_mapSurjective, IsZGroup.isZGroup, isZGroup_iff, pow_dvd_card_of_pow_dvd_card, card_eq_card_quotient_normalizer, smul_le, conj_eq_normalizer_conj_of_mem_centralizer, IsCyclic.normalizer_le_centralizer, exists_comap_eq_of_ker_isPGroup, card_eq_index_normalizer, IsZGroup.instIsCyclicSubtypeMemSubgroupOfFactPrime, card_coprime_index
unique_of_normal 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_coprime_index 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup Subgroup.index	—	IsPGroup.iff_card Subgroup.instFiniteSubtypeMem isPGroup' Nat.Prime.coprime_pow_of_not_dvd Fact.out not_dvd_index Subgroup.finiteIndex_of_finite
card_dvd_index 📖	mathematical	—	Nat.card Sylow Subgroup.index toSubgroup	—	Dvd.dvd.trans card_eq_index_normalizer dvd_rfl Subgroup.index_dvd_of_le Subgroup.le_normalizer
card_eq_card_quotient_normalizer 📖	mathematical	—	Nat.card Sylow HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.normalizer SetLike.coe Subgroup.instSetLike toSubgroup	—	Nat.card_congr
card_eq_index_normalizer 📖	mathematical	—	Nat.card Sylow Subgroup.index Subgroup.normalizer SetLike.coe Subgroup Subgroup.instSetLike toSubgroup	—	card_eq_card_quotient_normalizer
card_eq_multiplicity 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup Monoid.toPow Nat.instMonoid DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	—	IsPGroup.iff_card Subgroup.instFiniteSubtypeMem isPGroup' Nat.Prime.pow_dvd_iff_dvd_ordProj Fact.out LT.lt.ne' Nat.card_pos One.instNonempty Subgroup.card_subgroup_dvd_card pow_dvd_card_of_pow_dvd_card Nat.ordProj_dvd
card_normalizer_modEq_card 📖	mathematical	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid	Nat.ModEq Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe	—	Subgroup.le_normalizer Subgroup.card_eq_card_quotient_mul_card_subgroup Nat.card_congr pow_succ' Nat.ModEq.mul_right' card_quotient_normalizer_modEq_card_quotient
card_quotient_normalizer_modEq_card_quotient 📖	mathematical	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid	Nat.ModEq Nat.card HasQuotient.Quotient Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe Subgroup.toGroup QuotientGroup.instHasQuotientSubgroup Subgroup.comap Subgroup.subtype	—	Nat.card_congr Subtype.finite Nat.ModEq.symm IsPGroup.card_modEq_card_fixedPoints IsPGroup.of_card Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_of_finite
characteristic_of_normal 📖	mathematical	—	Subgroup.Characteristic toSubgroup	—	characteristic_of_subsingleton Unique.instSubsingleton
characteristic_of_subsingleton 📖	mathematical	—	Subgroup.Characteristic toSubgroup	—	Subgroup.characteristic_iff_map_eq Subgroup.pointwise_smul_def pointwise_smul_def
coe_comapOfInjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup MonoidHom.range	toSubgroup comapOfInjective Subgroup.comap	—	—
coe_comapOfKerIsPGroup 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup MonoidHom.range	toSubgroup comapOfKerIsPGroup Subgroup.comap	—	—
coe_mapSurjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	toSubgroup mapSurjective Subgroup.map	—	—
coe_ofCard 📖	mathematical	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	toSubgroup ofCard	—	—
coe_smul 📖	mathematical	—	SetLike.coe Sylow instSetLike SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Set Set.smulSet MulAut.instGroup MulAut.applyMulAction DFunLike.coe MonoidHom MonoidHom.instFunLike MulAut.conj	—	—
coe_subgroup_smul 📖	mathematical	—	toSubgroup Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Subgroup MulAut.instGroup Subgroup.pointwiseMulAction MulAut.applyMulDistribMulAction DFunLike.coe MonoidHom MonoidHom.instFunLike MulAut.conj	—	—
coe_subtype 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup	toSubgroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup subtype Subgroup.subgroupOf	—	—
conj_eq_normalizer_conj_of_mem 📖	mathematical	Sylow SetLike.instMembership instSetLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe toSubgroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	conj_eq_normalizer_conj_of_mem_centralizer Subgroup.le_centralizer
conj_eq_normalizer_conj_of_mem_centralizer 📖	mathematical	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.centralizer SetLike.coe Sylow instSetLike MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe toSubgroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Subgroup.le_centralizer_iff Subgroup.zpowers_le mul_assoc eq_inv_mul_iff_mul_eq eq_mul_inv_iff_mul_eq MulAction.exists_smul_eq isPretransitive_of_finite instFiniteSubtypeMemSubgroup smul_eq_iff_mem_normalizer subtype_injective smul_le smul_smul subtype.congr_simp smul_subtype Commute.right_comm Subtype.prop Subgroup.mem_zpowers mul_inv_rev inv_mul_cancel_right
dvd_card_of_dvd_card 📖	mathematical	Nat.card	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup	—	pow_dvd_card_of_pow_dvd_card pow_one
exists_comap_eq_of_injective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Sylow Subgroup.comap toSubgroup	—	exists_comap_eq_of_ker_isPGroup IsPGroup.ker_isPGroup_of_injective
exists_comap_eq_of_ker_isPGroup 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	Sylow Subgroup.comap toSubgroup	—	is_maximal' IsPGroup.comap_of_ker_isPGroup isPGroup' Subgroup.map_le_iff_le_comap IsPGroup.exists_le_sylow IsPGroup.map
exists_comap_subtype_eq 📖	mathematical	—	Sylow Subgroup.comap Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype toSubgroup	—	exists_comap_eq_of_injective Subtype.coe_injective
exists_subgroup_card_pow_prime 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card	Subgroup Nat.card SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid	—	exists_subgroup_card_pow_prime_le Subgroup.card_bot pow_zero
exists_subgroup_card_pow_prime_le 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Subgroup Nat.card SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	—
exists_subgroup_card_pow_prime_of_le_card 📖	mathematical	Nat.Prime IsPGroup Monoid.toPow Nat.instMonoid Nat.card	Subgroup Nat.card SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid	—	Nat.finite_of_card_ne_zero Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_pow sub_eq_zero_of_eq Nat.cast_zero Nat.cast_one Nat.Prime.pos IsPGroup.exists_card_eq exists_subgroup_card_pow_prime pow_dvd_pow Nat.Prime.one_lt
exists_subgroup_card_pow_succ 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Subgroup Nat.card SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	exists_eq_mul_left_of_dvd mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero LT.lt.ne' Nat.card_pos One.instNonempty Subgroup.instFiniteSubtypeMem Subgroup.card_eq_card_quotient_mul_card_subgroup pow_succ' mul_assoc mul_comm IsPGroup.card_modEq_card_fixedPoints IsPGroup.of_card Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_of_finite Nat.card_congr Subtype.finite dvd_mul_left Subgroup.normal_in_normalizer exists_prime_orderOf_dvd_card' Subgroup.instFiniteIndex_subgroupOf Subgroup.le_normalizer Nat.card_image_of_injective Subtype.val_injective pow_succ Nat.card_zpowers Nat.card_prod zpow_zero QuotientGroup.eq_one_iff
exists_subgroup_le_card_le 📖	mathematical	Nat.Prime IsPGroup Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Nat.card SetLike.instMembership Subgroup.instSetLike	—	exists_nat_pow_near Nat.instIsStrictOrderedRing instArchimedeanNat CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt exists_subgroup_le_card_pow_prime_of_le_card LE.le.trans pow_succ'
exists_subgroup_le_card_pow_prime_of_le_card 📖	mathematical	Nat.Prime IsPGroup Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Nat.card SetLike.instMembership Subgroup.instSetLike Monoid.toPow Nat.instMonoid	—	exists_subgroup_card_pow_prime_of_le_card IsPGroup.to_subgroup Subgroup.map_subtype_le Subgroup.subtype_injective Nat.card_congr
ext 📖	—	toSubgroup	—	—	—
ext_iff 📖	mathematical	—	toSubgroup	—	ext
finite_of_finiteIndex 📖	mathematical	—	Finite Sylow	—	finite_of_ker_is_pGroup Subgroup.normalCore_normal QuotientGroup.ker_mk' IsPGroup.to_le isPGroup' Subgroup.normalCore_le SetLike.instFinite Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_normalCore
finite_of_injective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Finite Sylow	—	finite_of_ker_is_pGroup IsPGroup.ker_isPGroup_of_injective
finite_of_ker_is_pGroup 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup	Finite Sylow	—	exists_comap_eq_of_ker_isPGroup Finite.of_injective ext
instFiniteQuotientSubgroupNormalizer 📖	mathematical	—	Finite HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.normalizer SetLike.coe Subgroup.instSetLike toSubgroup	—	Finite.of_equiv
instFiniteSubtypeMemSubgroup 📖	mathematical	—	Finite Sylow Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	—	finite_of_injective Subgroup.subtype_injective
instSubgroupClass 📖	mathematical	—	SubgroupClass Sylow Group.toDivInvMonoid instSetLike	—	Subgroup.mul_mem Subgroup.one_mem Subgroup.inv_mem
isPGroup' 📖	mathematical	—	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup Subgroup.toGroup	—	—
isPretransitive_of_finite 📖	mathematical	—	MulAction.IsPretransitive Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction	—	IsPGroup.sylow_mem_fixedPoints_iff isPGroup' is_maximal' ge_of_eq IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card Nat.Prime.not_dvd_one Fact.out Nat.modEq_zero_iff_dvd MulAction.mem_orbit_self Nat.card_unique Unique.instSubsingleton Set.eq_singleton_iff_unique_mem ext Nat.ModEq.symm IsPGroup.card_modEq_card_fixedPoints Subtype.finite
is_maximal' 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup	toSubgroup	—	—
mapSurjective_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Sylow mapSurjective	—	Finite.of_surjective nonempty Subgroup.map_le_iff_le_comap Subgroup.map_subtype_le IsPGroup.map isPGroup' Subgroup.index_map_subtype Subgroup.index_comap_of_surjective Nat.Prime.not_dvd_mul Fact.out not_dvd_index Subgroup.finiteIndex_of_finite Subgroup.instFiniteSubtypeMem ext_iff coe_mapSurjective is_maximal' Dvd.dvd.trans Subgroup.index_map_dvd
mem_fixedPoints_mul_left_cosets_iff_mem_normalizer 📖	mathematical	—	HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Set Set.instMembership MulAction.fixedPoints SetLike.instMembership Subgroup.instSetLike DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.mulLeftCosetsCompSubtypeVal Subgroup.normalizer SetLike.coe	—	MulAction.mem_fixedPoints' inv_mem_iff SubgroupClass.toInvMemClass Subgroup.instSubgroupClass Subgroup.mem_normalizer_fintype QuotientGroup.eq InvMemClass.inv_mem inv_inv mul_inv_rev Quotient.inductionOn' mul_mem_cancel_left mul_inv_cancel_left mul_assoc
ne_bot_of_dvd_card 📖	—	Nat.card	—	—	Nat.Prime.not_dvd_one Fact.out dvd_card_of_dvd_card Subgroup.card_bot
nonempty 📖	mathematical	—	Sylow	—	IsPGroup.exists_le_sylow IsPGroup.of_bot
normal_of_all_max_subgroups_normal 📖	mathematical	Subgroup.Normal	Subgroup.Normal toSubgroup	—	Subgroup.normalizer_eq_top_iff IsCoatomic.eq_top_or_exists_le_coatom IsStronglyCoatomic.toIsCoatomic instIsStronglyCoatomicOfWellFoundedGT Finite.to_wellFoundedGT SetLike.instFinite le_trans Subgroup.le_normalizer sup_of_le_right normalizer_sup_eq_top' instFiniteSubtypeMemSubgroup
normal_of_normalizerCondition 📖	mathematical	NormalizerCondition	Subgroup.Normal toSubgroup	—	Subgroup.normalizer_eq_top_iff normalizerCondition_iff_only_full_group_self_normalizing normalizer_normalizer
normal_of_normalizer_normal 📖	mathematical	—	Subgroup.Normal toSubgroup	—	Subgroup.normalizer_eq_top_iff normalizer_sup_eq_top' instFiniteSubtypeMemSubgroup Subgroup.le_normalizer sup_idem
normal_of_subsingleton 📖	mathematical	—	Subgroup.Normal toSubgroup	—	Subgroup.normal_of_characteristic characteristic_of_subsingleton
normalizer_normalizer 📖	mathematical	—	Subgroup.normalizer SetLike.coe Subgroup Subgroup.instSetLike toSubgroup	—	LE.le.trans Subgroup.le_normalizer normal_of_normalizer_normal instFiniteSubtypeMemSubgroup le_antisymm Subgroup.subgroupOf_normalizer_eq Subgroup.normal_subgroupOf_iff_le_normalizer coe_subtype Subgroup.normal_in_normalizer
normalizer_sup_eq_top 📖	mathematical	—	Subgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.normalizer SetLike.coe Subgroup.instSetLike Subgroup.map SetLike.instMembership Subgroup.toGroup Subgroup.subtype toSubgroup Top.top Subgroup.instTop	—	top_le_iff MulAction.exists_smul_eq isPretransitive_of_finite inv_mul_cancel_left sup_comm Subgroup.mul_mem_sup Subgroup.inv_mem MulEquiv.injective Subgroup.mem_map_iff_mem Subgroup.map_map Subgroup.pointwise_smul_def pointwise_smul_def ext_iff MonoidHom.map_mul MulAut.conjNormal_val SemigroupAction.mul_smul smul_def
normalizer_sup_eq_top' 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup	Subgroup SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.normalizer SetLike.coe Subgroup.instSetLike toSubgroup Top.top Subgroup.instTop	—	normalizer_sup_eq_top coe_subtype Subgroup.subgroupOf_map_subtype inf_of_le_left
not_dvd_index 📖	mathematical	—	Subgroup.index toSubgroup	—	finite_of_finiteIndex not_dvd_index' LT.lt.ne' Nat.card_pos Subgroup.finite_quotient_of_finiteIndex Subgroup.instFiniteIndex_subgroupOf
not_dvd_index' 📖	mathematical	—	Subgroup.index toSubgroup	—	Subgroup.relIndex_mul_index Subgroup.le_normalizer card_eq_index_normalizer Subgroup.normal_in_normalizer Nat.Prime.not_dvd_mul Fact.out not_dvd_card_sylow
orbit_eq_top 📖	mathematical	—	MulAction.orbit Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra	—	top_le_iff MulAction.exists_smul_eq isPretransitive_of_finite
pointwise_smul_def 📖	mathematical	—	toSubgroup Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction pointwiseMulAction Subgroup Subgroup.pointwiseMulAction	—	—
pow_dvd_card_of_pow_dvd_card 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup	—	Nat.Prime.coprime_pow_of_not_dvd Fact.out not_dvd_index Subgroup.finiteIndex_of_finite Subgroup.index_mul_card
prime_dvd_card_quotient_normalizer 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Nat.card HasQuotient.Quotient Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe Subgroup.toGroup QuotientGroup.instHasQuotientSubgroup Subgroup.comap Subgroup.subtype	—	exists_eq_mul_left_of_dvd mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero Nat.instIsCancelMulZero LT.lt.ne' Nat.card_pos One.instNonempty Subgroup.instFiniteSubtypeMem Subgroup.card_eq_card_quotient_mul_card_subgroup pow_succ' mul_assoc mul_comm Nat.ModEq.symm card_quotient_normalizer_modEq_card_quotient dvd_mul_left
prime_pow_dvd_card_normalizer 📖	mathematical	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Monoid.toPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe	—	Nat.modEq_zero_iff_dvd Nat.ModEq.trans card_normalizer_modEq_card Dvd.dvd.modEq_zero_nat
smul_def 📖	mathematical	—	Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction MulAut MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulAut.instGroup pointwiseMulAction MulAut.applyMulDistribMulAction DFunLike.coe MonoidHom MonoidHom.instFunLike MulAut.conj	—	—
smul_eq_iff_mem_normalizer 📖	mathematical	—	Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.normalizer SetLike.coe toSubgroup	—	SetLike.ext_iff inv_mem_iff SubgroupClass.toInvMemClass Subgroup.instSubgroupClass Subgroup.mem_normalizer_iff inv_inv mul_assoc inv_mul_cancel_left inv_mul_cancel mul_one MulAut.apply_inv_self
smul_eq_of_normal 📖	mathematical	—	Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction	—	Subgroup.normalizer_eq_top
smul_le 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup SetLike.instMembership Subgroup.instSetLike Sylow SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MulAction.toSemigroupAction Subgroup.instMulAction mulAction	—	Subgroup.conj_smul_le_of_le
smul_subtype 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup	Subgroup SetLike.instMembership Subgroup.instSetLike Sylow Subgroup.toGroup SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction mulAction subtype Subgroup.instMulAction smul_le	—	ext smul_le Subgroup.conj_smul_subgroupOf
stabilizer_eq_normalizer 📖	mathematical	—	MulAction.stabilizer Sylow mulAction Subgroup.normalizer SetLike.coe Subgroup Subgroup.instSetLike toSubgroup	—	Subgroup.ext
subtype_injective 📖	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup subtype	—	—	SetLike.ext_iff

(root)

Definitions

Name	Category	Theorems
Sylow 📖	CompData	37 math math: Sylow.pointwise_smul_def, IsPGroup.sylow_mem_fixedPoints_iff, Sylow.coe_smul, Sylow.card_dvd_index, Sylow.smul_eq_iff_mem_normalizer, alternatingGroup.subsingleton_two_sylow, MonoidHom.transferSylow_restrict_eq_pow, Sylow.stabilizer_eq_normalizer, Sylow.mapSurjective_surjective, Sylow.orbit_eq_top, Subgroup.sylow_mem_fixedPoints_iff, Sylow.exists_comap_eq_of_injective, Sylow.finite_of_finiteIndex, Sylow.nonempty, Sylow.smul_eq_of_normal, Sylow.finite_of_ker_is_pGroup, Sylow.normalizer_le_centralizer_or_le_commutator, IsPGroup.exists_le_sylow, isNilpotent_of_finite_tfae, alternatingGroup.coe_two_sylow_of_card_eq_four, IsPGroup.mem_toSylow, card_sylow_modEq_one, Sylow.instSubgroupClass, Sylow.coe_subgroup_smul, Sylow.smul_subtype, Sylow.isPretransitive_of_finite, Sylow.exists_comap_subtype_eq, Subgroup.ker_restrict_transferFocal_eq_focalSubgroupOf, not_dvd_card_sylow, Sylow.card_eq_card_quotient_normalizer, Sylow.smul_le, Sylow.smul_def, IsCyclic.normalizer_le_centralizer, Sylow.exists_comap_eq_of_ker_isPGroup, Sylow.card_eq_index_normalizer, Sylow.finite_of_injective, Sylow.instFiniteSubtypeMemSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_sylow_modEq_one 📖	mathematical	—	Nat.ModEq Nat.card Sylow	—	Sylow.nonempty Set.ext IsPGroup.sylow_mem_fixedPoints_iff Sylow.isPGroup' Sylow.is_maximal' ge_of_eq Sylow.ext_iff Set.mem_singleton_iff Nat.card_eq_fintype_card Fintype.card_unique Nat.ModEq.trans IsPGroup.card_modEq_card_fixedPoints Nat.ModEq.refl
not_dvd_card_sylow 📖	mathematical	—	Nat.card Sylow	—	Nat.Prime.ne_one Fact.out Nat.modEq_iff_dvd' zero_le_one Nat.instZeroLEOneClass Nat.ModEq.trans Nat.ModEq.symm Nat.modEq_zero_iff_dvd card_sylow_modEq_one

---

← Back to Index