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_injective, finite_of_ker_is_pGroup, instFiniteQuotientSubgroupNormalizerOfFactPrime, 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	72
Total	92

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	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.instMin Subgroup.normalizer 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 Sylow.instSetLike toSylow	—	—
sylow_mem_fixedPoints_iff 📖	mathematical	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup	Sylow Set Set.instMembership MulAction.fixedPoints DivInvMonoid.toMonoid Group.toDivInvMonoid 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 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	6 math math: coe_smul, normalizer_le_centralizer_or_le_commutator, alternatingGroup.coe_two_sylow_of_card_eq_four, IsPGroup.mem_toSylow, instSubgroupClass, 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	46 math math: isPGroup', not_dvd_index', IsCyclic.isComplement', pointwise_smul_def, IsPGroup.sylow_mem_fixedPoints_iff, normalizer_normalizer, alternatingGroup.card_two_sylow_of_card_eq_four, normal_of_normalizerCondition, card_dvd_index, coe_ofCard, smul_eq_iff_mem_normalizer, normal_of_all_max_subgroups_normal, not_dvd_index, ext_iff, stabilizer_eq_normalizer, normal_of_subsingleton, characteristic_of_subsingleton, 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, IsPGroup.exists_le_sylow, isNilpotent_of_finite_tfae, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four, IsPGroup.toSylow_coe, card_eq_multiplicity, coe_subgroup_smul, normalizer_sup_eq_top, dvd_card_of_dvd_card, exists_comap_subtype_eq, normal_of_normalizer_normal, IsPGroup.inf_normalizer_sylow, coe_mapSurjective, IsZGroup.isZGroup, instFiniteQuotientSubgroupNormalizerOfFactPrime, isZGroup_iff, pow_dvd_card_of_pow_dvd_card, card_eq_card_quotient_normalizer, 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 SetLike.instFinite 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 toSubgroup	—	Nat.card_congr
card_eq_index_normalizer 📖	mathematical	—	Nat.card Sylow Subgroup.index Subgroup.normalizer toSubgroup	—	card_eq_card_quotient_normalizer
card_eq_multiplicity 📖	mathematical	—	Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup Monoid.toNatPow 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.toNatPow Nat.instMonoid	Nat.ModEq Subgroup.normalizer	—	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.toNatPow Nat.instMonoid	Nat.ModEq HasQuotient.Quotient Subgroup.normalizer 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	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	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.toNatPow 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	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 Subgroup.instSetLike Subgroup.normalizer toSubgroup	—	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.normalizer toSubgroup	—	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	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	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	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	—	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.toNatPow Nat.instMonoid Nat.card	Subgroup SetLike.instMembership Subgroup.instSetLike	—	exists_subgroup_card_pow_prime_le Subgroup.card_bot pow_zero
exists_subgroup_card_pow_prime_le 📖	mathematical	Monoid.toNatPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	—
exists_subgroup_card_pow_prime_of_le_card 📖	mathematical	Nat.Prime IsPGroup Monoid.toNatPow Nat.instMonoid Nat.card	Subgroup SetLike.instMembership Subgroup.instSetLike	—	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.toNatPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	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	Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	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.toNatPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder	—	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_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
instFiniteQuotientSubgroupNormalizerOfFactPrime 📖	mathematical	—	Finite HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.normalizer 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' 📖	—	IsPGroup Subgroup SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder 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 instFiniteSubtypeMemSubgroup SetLike.instFinite 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	—	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	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 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 Subgroup.map SetLike.instMembership Subgroup.instSetLike 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	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice Subgroup.normalizer 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	—	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.toNatPow Nat.instMonoid Nat.card	Subgroup SetLike.instMembership Subgroup.instSetLike toSubgroup	—	Nat.Prime.coprime_pow_of_not_dvd Fact.out not_dvd_index SetLike.instFinite Subgroup.finiteIndex_of_finite Subgroup.index_mul_card
prime_dvd_card_quotient_normalizer 📖	mathematical	Monoid.toNatPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	HasQuotient.Quotient Subgroup.normalizer 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.toNatPow Nat.instMonoid Nat.card Subgroup SetLike.instMembership Subgroup.instSetLike	Subgroup.normalizer	—	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 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	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	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 toSubgroup	—	Subgroup.ext
subtype_injective 📖	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder toSubgroup subtype	—	—	SetLike.ext_iff

(root)

Definitions

Name	Category	Theorems
Sylow 📖	CompData	30 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, Sylow.stabilizer_eq_normalizer, Sylow.mapSurjective_surjective, Sylow.orbit_eq_top, Subgroup.sylow_mem_fixedPoints_iff, Sylow.nonempty, Sylow.smul_eq_of_normal, Sylow.finite_of_ker_is_pGroup, Sylow.normalizer_le_centralizer_or_le_commutator, 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, not_dvd_card_sylow, Sylow.card_eq_card_quotient_normalizer, Sylow.smul_le, Sylow.smul_def, IsCyclic.normalizer_le_centralizer, 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