Nilpotent

📁 Source: Mathlib/GroupTheory/Nilpotent.lean

Statistics

Metric	Count
Definitions IsNilpotent, IsVirtuallyNilpotent, nilpotencyClass, IsAscendingCentralSeries, IsDescendingCentralSeries, commGroupOfNilpotencyClass, lowerCentralSeries, upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep	10
Theorems isNilpotent, nilpotencyClass_le_one, isVirtuallyNilpotent, nilpotent, nilpotent', isNilpotent_congr, isNilpotent_iff, isNilpotent_of_subsingleton, isNilpotent_top, to_isSolvable, isNilpotent, isNilpotent, nilpotencyClass_le, ascending_central_series_le_upper, comap_upperCentralSeries, comap_upperCentralSeries_quotient_center, derived_le_lower_central, descending_central_series_ge_lower, instCharacteristicLowerCentralSeries, instCharacteristicUpperCentralSeries, instCharacteristicUpperCentralSeriesStep, isNilpotent_of_finite_tfae, isNilpotent_of_ker_le_center, isNilpotent_of_product_of_sylow_group, isNilpotent_pi, isNilpotent_pi_of_bounded_class, isNilpotent_prod, is_ascending_rev_series_of_is_descending, is_descending_rev_series_of_is_ascending, least_ascending_central_series_length_eq_nilpotencyClass, least_descending_central_series_length_eq_nilpotencyClass, map, lowerCentralSeries_antitone, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_isDescendingCentralSeries, lowerCentralSeries_length_eq_nilpotencyClass, lowerCentralSeries_map_subtype_le, lowerCentralSeries_nilpotencyClass, lowerCentralSeries_one, lowerCentralSeries_pi_le, lowerCentralSeries_pi_of_finite, lowerCentralSeries_prod, lowerCentralSeries_succ, lowerCentralSeries_succ_eq_bot, lowerCentralSeries_zero, mem_lowerCentralSeries_succ_iff, mem_upperCentralSeriesStep, mem_upperCentralSeries_succ_iff, nilpotencyClass_eq_quotient_center_plus_one, nilpotencyClass_le_of_ker_le_center, nilpotencyClass_le_of_surjective, nilpotencyClass_pi, nilpotencyClass_prod, nilpotencyClass_quotient_center, nilpotencyClass_quotient_le, nilpotencyClass_zero_iff_subsingleton, nilpotent_center_quotient_ind, nilpotent_iff_finite_ascending_central_series, nilpotent_iff_finite_descending_central_series, nilpotent_iff_lowerCentralSeries, nilpotent_of_mulEquiv, nilpotent_of_surjective, nilpotent_quotient_of_nilpotent, normalizerCondition_of_isNilpotent, of_quotient_center_nilpotent, map, upperCentralSeriesStep_eq_comap_center, upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_isAscendingCentralSeries, upperCentralSeries_mono, upperCentralSeries_nilpotencyClass, upperCentralSeries_one, upperCentralSeries_zero	73
Total	83

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent 📖	mathematical	—	Group.IsNilpotent toGroup	—	upperCentralSeries_one center_eq_top
nilpotencyClass_le_one 📖	mathematical	—	Group.nilpotencyClass toGroup isNilpotent	—	isNilpotent upperCentralSeries_eq_top_iff_nilpotencyClass_le upperCentralSeries_one center_eq_top

Group

Definitions

Name	Category	Theorems
IsNilpotent 📖	CompData	22 math math: isNilpotent_congr, isNilpotent_iff, CommGroup.isNilpotent, least_ascending_central_series_length_eq_nilpotencyClass, least_descending_central_series_length_eq_nilpotencyClass, of_quotient_center_nilpotent, nilpotent_iff_lowerCentralSeries, isNilpotent_prod, isNilpotent_of_finite_tfae, isNilpotent_of_product_of_sylow_group, Subgroup.isNilpotent, nilpotent_iff_finite_descending_central_series, nilpotent_of_surjective, isNilpotent_top, isNilpotent_of_subsingleton, isNilpotent_of_ker_le_center, IsPGroup.isNilpotent, frattini_nilpotent, lowerCentralSeries_length_eq_nilpotencyClass, nilpotent_of_mulEquiv, nilpotent_quotient_of_nilpotent, nilpotent_iff_finite_ascending_central_series
IsVirtuallyNilpotent 📖	MathDef	1 math math: IsNilpotent.isVirtuallyNilpotent
nilpotencyClass 📖	CompOp	17 math math: nilpotencyClass_quotient_center, least_ascending_central_series_length_eq_nilpotencyClass, nilpotencyClass_zero_iff_subsingleton, least_descending_central_series_length_eq_nilpotencyClass, upperCentralSeries_nilpotencyClass, nilpotencyClass_pi, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_nilpotencyClass, nilpotencyClass_quotient_le, upperCentralSeries_eq_top_iff_nilpotencyClass_le, CommGroup.nilpotencyClass_le_one, nilpotencyClass_le_of_ker_le_center, nilpotencyClass_eq_quotient_center_plus_one, nilpotencyClass_le_of_surjective, nilpotencyClass_prod, lowerCentralSeries_length_eq_nilpotencyClass, Subgroup.nilpotencyClass_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_congr 📖	mathematical	—	IsNilpotent	—	Subgroup.comap_top MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass comap_upperCentralSeries
isNilpotent_iff 📖	mathematical	—	IsNilpotent upperCentralSeries Top.top Subgroup Subgroup.instTop	—	—
isNilpotent_of_subsingleton 📖	mathematical	—	IsNilpotent	—	nilpotent_iff_lowerCentralSeries Unique.instSubsingleton
isNilpotent_top 📖	mathematical	—	IsNilpotent Subgroup SetLike.instMembership Subgroup.instSetLike Top.top Subgroup.instTop Subgroup.toGroup	—	isNilpotent_congr

Group.IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isVirtuallyNilpotent 📖	mathematical	—	Group.IsVirtuallyNilpotent	—	Subgroup.instFiniteIndexTop
nilpotent 📖	mathematical	—	upperCentralSeries Top.top Subgroup Subgroup.instTop	—	nilpotent'
nilpotent' 📖	mathematical	—	upperCentralSeries Top.top Subgroup Subgroup.instTop	—	—

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_isSolvable 📖	mathematical	—	IsSolvable	—	nilpotent_iff_lowerCentralSeries eq_bot_iff derived_le_lower_central

IsPGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent 📖	mathematical	IsPGroup	Group.IsNilpotent	—	nonempty_fintype Fintype.induction_subsingleton_or_nontrivial Group.isNilpotent_of_subsingleton Subgroup.card_eq_card_quotient_mul_card_subgroup Nat.card_eq_fintype_card lt_mul_of_one_lt_right LinearOrderedCommMonoidWithZero.toPosMulStrictMono Fintype.card_pos_iff One.instNonempty Subgroup.instNormalCenter Subgroup.one_lt_card_iff_ne_bot Subgroup.instFiniteSubtypeMem Finite.of_fintype ne_of_gt bot_lt_center to_quotient of_quotient_center_nilpotent

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent 📖	mathematical	—	Group.IsNilpotent Subgroup SetLike.instMembership instSetLike toGroup	—	nilpotent_iff_lowerCentralSeries lowerCentralSeries_map_subtype_le eq_bot_iff instIsConcreteLE
nilpotencyClass_le 📖	mathematical	—	Group.nilpotencyClass Subgroup SetLike.instMembership instSetLike toGroup isNilpotent	—	isNilpotent nilpotent_iff_lowerCentralSeries lowerCentralSeries_length_eq_nilpotencyClass Nat.find_mono lowerCentralSeries_map_subtype_le eq_bot_iff instIsConcreteLE

(root)

Definitions

Name	Category	Theorems
IsAscendingCentralSeries 📖	MathDef	4 math math: least_ascending_central_series_length_eq_nilpotencyClass, upperCentralSeries_isAscendingCentralSeries, nilpotent_iff_finite_ascending_central_series, is_ascending_rev_series_of_is_descending
IsDescendingCentralSeries 📖	MathDef	4 math math: lowerCentralSeries_isDescendingCentralSeries, is_descending_rev_series_of_is_ascending, least_descending_central_series_length_eq_nilpotencyClass, nilpotent_iff_finite_descending_central_series
commGroupOfNilpotencyClass 📖	CompOp	—
lowerCentralSeries 📖	CompOp	18 math math: lowerCentralSeries_isDescendingCentralSeries, lowerCentralSeries_antitone, descending_central_series_ge_lower, nilpotent_iff_lowerCentralSeries, mem_lowerCentralSeries_succ_iff, lowerCentralSeries_one, lowerCentralSeries_pi_le, lowerCentralSeries.map, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_succ, lowerCentralSeries_map_subtype_le, derived_le_lower_central, lowerCentralSeries_nilpotencyClass, lowerCentralSeries_zero, lowerCentralSeries_pi_of_finite, lowerCentralSeries_prod, lowerCentralSeries_length_eq_nilpotencyClass, instCharacteristicLowerCentralSeries
upperCentralSeries 📖	CompOp	15 math math: Group.isNilpotent_iff, upperCentralSeries_mono, Group.IsNilpotent.nilpotent', upperCentralSeries.map, upperCentralSeries_zero, comap_upperCentralSeries, upperCentralSeries_nilpotencyClass, comap_upperCentralSeries_quotient_center, mem_upperCentralSeries_succ_iff, instCharacteristicUpperCentralSeries, upperCentralSeries_isAscendingCentralSeries, upperCentralSeries_one, upperCentralSeries_eq_top_iff_nilpotencyClass_le, ascending_central_series_le_upper, Group.IsNilpotent.nilpotent
upperCentralSeriesAux 📖	CompOp	—
upperCentralSeriesStep 📖	CompOp	3 math math: mem_upperCentralSeriesStep, instCharacteristicUpperCentralSeriesStep, upperCentralSeriesStep_eq_comap_center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ascending_central_series_le_upper 📖	mathematical	IsAscendingCentralSeries	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder upperCentralSeries	—	le_refl mem_upperCentralSeries_succ_iff
comap_upperCentralSeries 📖	mathematical	—	Subgroup.comap MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass upperCentralSeries	—	MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass MulEquiv.injective Subgroup.ext Equiv.forall_congr_right map_mul MonoidHomClass.toMulHomClass map_inv
comap_upperCentralSeries_quotient_center 📖	mathematical	—	Subgroup.comap HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.center QuotientGroup.Quotient.group Subgroup.instNormalCenter QuotientGroup.mk' upperCentralSeries	—	Subgroup.instNormalCenter QuotientGroup.ker_mk' upperCentralSeries_one Subgroup.normal_of_characteristic instCharacteristicUpperCentralSeries Subgroup.normal_comap upperCentralSeriesStep_eq_comap_center QuotientGroup.comap_comap_center symm IsEquiv.toSymm eq_isEquiv
derived_le_lower_central 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder derivedSeries lowerCentralSeries	—	Subgroup.commutator_mono
descending_central_series_ge_lower 📖	mathematical	IsDescendingCentralSeries	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder lowerCentralSeries	—	le_refl Subgroup.commutator_le
instCharacteristicLowerCentralSeries 📖	mathematical	—	Subgroup.Characteristic lowerCentralSeries	—	lowerCentralSeries.eq_def Subgroup.commutator_characteristic Subgroup.topCharacteristic
instCharacteristicUpperCentralSeries 📖	mathematical	—	Subgroup.Characteristic upperCentralSeries	—	—
instCharacteristicUpperCentralSeriesStep 📖	mathematical	—	Subgroup.Characteristic upperCentralSeriesStep	—	Subgroup.centerCharacteristic Subgroup.normal_of_characteristic upperCentralSeriesStep_eq_comap_center
isNilpotent_of_finite_tfae 📖	mathematical	—	List.TFAE Group.IsNilpotent NormalizerCondition MulEquiv Pi.instMul Finset SetLike.instMembership Finset.instSetLike Nat.primeFactors Nat.card Sylow Subgroup Subgroup.instSetLike Sylow.toSubgroup Subgroup.mul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	normalizerCondition_of_isNilpotent Subgroup.NormalizerCondition.normal_of_coatom Sylow.normal_of_all_max_subgroups_normal SetLike.instFinite isNilpotent_of_product_of_sylow_group List.tfae_of_cycle
isNilpotent_of_ker_le_center 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.center	Group.IsNilpotent	—	nilpotent_iff_lowerCentralSeries lowerCentralSeries_succ_eq_bot le_trans Subgroup.map_eq_bot_iff eq_bot_iff lowerCentralSeries.map
isNilpotent_of_product_of_sylow_group 📖	mathematical	—	Group.IsNilpotent	—	IsPGroup.isNilpotent Subgroup.instFiniteSubtypeMem Nat.prime_of_mem_primeFactors Sylow.isPGroup' nilpotent_of_mulEquiv isNilpotent_pi Finite.of_fintype SetLike.instFinite
isNilpotent_pi 📖	mathematical	Group.IsNilpotent	Pi.group	—	nonempty_fintype nilpotent_iff_lowerCentralSeries lowerCentralSeries_pi_of_finite Subgroup.pi_eq_bot_iff lowerCentralSeries_eq_bot_iff_nilpotencyClass_le Finset.le_sup Finset.mem_univ
isNilpotent_pi_of_bounded_class 📖	mathematical	Group.IsNilpotent Group.nilpotencyClass	Pi.group	—	nilpotent_iff_lowerCentralSeries eq_bot_iff le_trans lowerCentralSeries_pi_le Subgroup.pi_eq_bot_iff lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
isNilpotent_prod 📖	mathematical	—	Group.IsNilpotent Prod.instGroup	—	nilpotent_iff_lowerCentralSeries lowerCentralSeries_prod lowerCentralSeries_eq_bot_iff_nilpotencyClass_le le_max_left le_max_right Subgroup.bot_prod_bot
is_ascending_rev_series_of_is_descending 📖	mathematical	Bot.bot Subgroup Subgroup.instBot IsDescendingCentralSeries	IsAscendingCentralSeries	—	tsub_eq_zero_iff_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Subgroup.mem_top tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
is_descending_rev_series_of_is_ascending 📖	mathematical	Top.top Subgroup Subgroup.instTop IsAscendingCentralSeries	IsDescendingCentralSeries	—	one_mul one_zpow mul_one add_neg_cancel zpow_zero Subgroup.one_mem Subgroup.mem_bot tsub_eq_zero_of_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
least_ascending_central_series_length_eq_nilpotencyClass 📖	mathematical	—	Nat.find IsAscendingCentralSeries Subgroup Top.top Subgroup.instTop Group.IsNilpotent nilpotent_iff_finite_ascending_central_series Group.nilpotencyClass	—	le_antisymm nilpotent_iff_finite_ascending_central_series Nat.find_mono upperCentralSeries_isAscendingCentralSeries Group.IsNilpotent.nilpotent top_le_iff ascending_central_series_le_upper
least_descending_central_series_length_eq_nilpotencyClass 📖	mathematical	—	Nat.find IsDescendingCentralSeries Subgroup Bot.bot Subgroup.instBot Group.IsNilpotent nilpotent_iff_finite_descending_central_series Group.nilpotencyClass	—	nilpotent_iff_finite_descending_central_series nilpotent_iff_finite_ascending_central_series least_ascending_central_series_length_eq_nilpotencyClass le_antisymm Nat.find_mono is_descending_rev_series_of_is_ascending tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub is_ascending_rev_series_of_is_descending
lowerCentralSeries_antitone 📖	mathematical	—	Antitone Subgroup Nat.instPreorder PartialOrder.toPreorder Subgroup.instPartialOrder lowerCentralSeries	—	antitone_nat_of_succ_le Subgroup.closure_induction mul_assoc MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.Normal.conj_mem Subgroup.normal_of_characteristic instCharacteristicLowerCentralSeries InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.one_mem
lowerCentralSeries_eq_bot_iff_nilpotencyClass_le 📖	mathematical	—	lowerCentralSeries Bot.bot Subgroup Subgroup.instBot Group.nilpotencyClass	—	nilpotent_iff_lowerCentralSeries lowerCentralSeries_length_eq_nilpotencyClass Nat.find_le eq_bot_iff lowerCentralSeries_nilpotencyClass lowerCentralSeries_antitone
lowerCentralSeries_isDescendingCentralSeries 📖	mathematical	—	IsDescendingCentralSeries lowerCentralSeries	—	Subgroup.commutator_mem_commutator Subgroup.mem_top
lowerCentralSeries_length_eq_nilpotencyClass 📖	mathematical	—	Nat.find Subgroup lowerCentralSeries Bot.bot Subgroup.instBot Group.IsNilpotent nilpotent_iff_lowerCentralSeries Group.nilpotencyClass	—	nilpotent_iff_lowerCentralSeries nilpotent_iff_finite_descending_central_series least_descending_central_series_length_eq_nilpotencyClass le_antisymm Nat.find_mono le_bot_iff descending_central_series_ge_lower lowerCentralSeries_isDescendingCentralSeries
lowerCentralSeries_map_subtype_le 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.map SetLike.instMembership Subgroup.instSetLike Subgroup.toGroup Subgroup.subtype lowerCentralSeries	—	lowerCentralSeries_succ MonoidHom.map_closure Subgroup.closure_mono Subgroup.mem_map
lowerCentralSeries_nilpotencyClass 📖	mathematical	—	lowerCentralSeries Group.nilpotencyClass Bot.bot Subgroup Subgroup.instBot	—	nilpotent_iff_lowerCentralSeries lowerCentralSeries_length_eq_nilpotencyClass Nat.find_spec
lowerCentralSeries_one 📖	mathematical	—	lowerCentralSeries commutator	—	—
lowerCentralSeries_pi_le 📖	mathematical	—	Subgroup Pi.group Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder lowerCentralSeries Subgroup.pi Set.univ	—	Subgroup.pi_top Subgroup.commutator_mono le_refl Subgroup.commutator_pi_pi_le
lowerCentralSeries_pi_of_finite 📖	mathematical	—	lowerCentralSeries Pi.group Subgroup.pi Set.univ	—	Subgroup.pi_top Subgroup.commutator_pi_pi_of_finite
lowerCentralSeries_prod 📖	mathematical	—	lowerCentralSeries Prod.instGroup Subgroup.prod	—	Subgroup.top_prod_top Subgroup.commutator_prod_prod
lowerCentralSeries_succ 📖	mathematical	—	lowerCentralSeries Subgroup.closure setOf Subgroup SetLike.instMembership Subgroup.instSetLike Top.top Subgroup.instTop MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
lowerCentralSeries_succ_eq_bot 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder lowerCentralSeries Subgroup.center	Bot.bot Subgroup.instBot	—	lowerCentralSeries_succ Subgroup.closure_eq_bot_iff Set.subset_singleton_iff mul_assoc mul_inv_rev mul_inv_eq_one Subgroup.mem_center_iff
lowerCentralSeries_zero 📖	mathematical	—	lowerCentralSeries Top.top Subgroup Subgroup.instTop	—	—
mem_lowerCentralSeries_succ_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike lowerCentralSeries Subgroup.closure setOf Top.top Subgroup.instTop MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mem_upperCentralSeriesStep 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike upperCentralSeriesStep MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mem_upperCentralSeries_succ_iff 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike upperCentralSeries MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
nilpotencyClass_eq_quotient_center_plus_one 📖	mathematical	—	Group.nilpotencyClass HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.center QuotientGroup.Quotient.group Subgroup.instNormalCenter nilpotent_quotient_of_nilpotent	—	Subgroup.instNormalCenter nilpotent_quotient_of_nilpotent nilpotencyClass_quotient_center false_of_nontrivial_of_subsingleton nilpotencyClass_zero_iff_subsingleton add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
nilpotencyClass_le_of_ker_le_center 📖	mathematical	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder MonoidHom.ker Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.center	Group.nilpotencyClass isNilpotent_of_ker_le_center	—	isNilpotent_of_ker_le_center nilpotent_iff_lowerCentralSeries lowerCentralSeries_length_eq_nilpotencyClass Nat.find_min' lowerCentralSeries_succ_eq_bot le_trans Subgroup.map_eq_bot_iff eq_bot_iff lowerCentralSeries.map lowerCentralSeries_nilpotencyClass
nilpotencyClass_le_of_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Group.nilpotencyClass nilpotent_of_surjective	—	Nat.find_mono eq_top_iff symm IsEquiv.toSymm eq_isEquiv MonoidHom.range_eq_top_of_surjective MonoidHom.range_eq_map upperCentralSeries.map Group.IsNilpotent.nilpotent nilpotent_of_surjective
nilpotencyClass_pi 📖	mathematical	Group.IsNilpotent	Group.nilpotencyClass Pi.group isNilpotent_pi Finite.of_fintype Finset.sup Lattice.toSemilatticeSup Nat.instLattice Nat.instOrderBot Finset.univ	—	eq_of_forall_ge_iff isNilpotent_pi Finite.of_fintype lowerCentralSeries_pi_of_finite
nilpotencyClass_prod 📖	mathematical	—	Group.nilpotencyClass Prod.instGroup isNilpotent_prod	—	eq_of_forall_ge_iff isNilpotent_prod lowerCentralSeries_prod
nilpotencyClass_quotient_center 📖	mathematical	—	Group.nilpotencyClass HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup Subgroup.center QuotientGroup.Quotient.group Subgroup.instNormalCenter nilpotent_quotient_of_nilpotent	—	Subgroup.instNormalCenter nilpotent_quotient_of_nilpotent zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Quotient.instSubsingletonQuotient le_antisymm upperCentralSeries_eq_top_iff_nilpotencyClass_le Subgroup.comap_injective Quot.mk_surjective comap_upperCentralSeries_quotient_center Subgroup.comap_top upperCentralSeries_nilpotencyClass le_of_add_le_add_right IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid nilpotencyClass_le_of_ker_le_center le_of_eq QuotientGroup.ker_mk' add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd
nilpotencyClass_quotient_le 📖	mathematical	—	Group.nilpotencyClass HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group nilpotent_quotient_of_nilpotent	—	nilpotencyClass_le_of_surjective QuotientGroup.mk_surjective
nilpotencyClass_zero_iff_subsingleton 📖	mathematical	—	Group.nilpotencyClass	—	Group.IsNilpotent.nilpotent Group.nilpotencyClass.eq_1 Nat.find_eq_zero upperCentralSeries_zero subsingleton_iff_bot_eq_top Subgroup.subsingleton_iff
nilpotent_center_quotient_ind 📖	—	Group.isNilpotent_of_subsingleton	—	—	Group.isNilpotent_of_subsingleton Subgroup.instNormalCenter nilpotent_quotient_of_nilpotent nilpotencyClass_zero_iff_subsingleton nilpotencyClass_quotient_center add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
nilpotent_iff_finite_ascending_central_series 📖	mathematical	—	Group.IsNilpotent IsAscendingCentralSeries Top.top Subgroup Subgroup.instTop	—	upperCentralSeries_isAscendingCentralSeries eq_top_iff ascending_central_series_le_upper
nilpotent_iff_finite_descending_central_series 📖	mathematical	—	Group.IsNilpotent IsDescendingCentralSeries Bot.bot Subgroup Subgroup.instBot	—	nilpotent_iff_finite_ascending_central_series is_descending_rev_series_of_is_ascending tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub is_ascending_rev_series_of_is_descending
nilpotent_iff_lowerCentralSeries 📖	mathematical	—	Group.IsNilpotent lowerCentralSeries Bot.bot Subgroup Subgroup.instBot	—	nilpotent_iff_finite_descending_central_series eq_bot_iff descending_central_series_ge_lower lowerCentralSeries_isDescendingCentralSeries
nilpotent_of_mulEquiv 📖	mathematical	—	Group.IsNilpotent	—	nilpotent_of_surjective MulEquiv.surjective
nilpotent_of_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Group.IsNilpotent	—	eq_top_iff symm IsEquiv.toSymm eq_isEquiv MonoidHom.range_eq_top_of_surjective MonoidHom.range_eq_map upperCentralSeries.map
nilpotent_quotient_of_nilpotent 📖	mathematical	—	Group.IsNilpotent HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group	—	nilpotent_of_surjective QuotientGroup.mk_surjective
normalizerCondition_of_isNilpotent 📖	mathematical	—	NormalizerCondition	—	normalizerCondition_iff_only_full_group_self_normalizing nilpotent_center_quotient_ind Unique.instSubsingleton Subgroup.instNormalCenter LE.le.trans Subgroup.center_le_normalizer le_of_eq QuotientGroup.ker_mk' Quot.mk_surjective Subgroup.comap_injective Subgroup.comap_normalizer_eq_of_surjective Subgroup.comap_map_eq_self Subgroup.map_injective_of_ker_le le_top symm IsEquiv.toSymm eq_isEquiv Subgroup.map_top_of_surjective
of_quotient_center_nilpotent 📖	mathematical	—	Group.IsNilpotent	—	Subgroup.instNormalCenter Group.IsNilpotent.nilpotent Subgroup.comap_top
upperCentralSeriesStep_eq_comap_center 📖	mathematical	—	upperCentralSeriesStep Subgroup.comap HasQuotient.Quotient Subgroup QuotientGroup.instHasQuotientSubgroup QuotientGroup.Quotient.group QuotientGroup.mk' Subgroup.center	—	Subgroup.ext Subgroup.mem_comap Subgroup.mem_center_iff QuotientGroup.coe_mk' QuotientGroup.mk_mul QuotientGroup.eq_iff_div_mem div_eq_mul_inv mul_inv_rev mul_assoc
upperCentralSeries_eq_top_iff_nilpotencyClass_le 📖	mathematical	—	upperCentralSeries Top.top Subgroup Subgroup.instTop Group.nilpotencyClass	—	Nat.find_le Group.IsNilpotent.nilpotent eq_top_iff upperCentralSeries_nilpotencyClass upperCentralSeries_mono
upperCentralSeries_isAscendingCentralSeries 📖	mathematical	—	IsAscendingCentralSeries upperCentralSeries	—	—
upperCentralSeries_mono 📖	mathematical	—	Monotone Subgroup Nat.instPreorder PartialOrder.toPreorder Subgroup.instPartialOrder upperCentralSeries	—	monotone_nat_of_le_succ mul_assoc MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubgroupClass.toSubmonoidClass Subgroup.instSubgroupClass Subgroup.Normal.conj_mem Subgroup.normal_of_characteristic instCharacteristicUpperCentralSeries InvMemClass.inv_mem SubgroupClass.toInvMemClass
upperCentralSeries_nilpotencyClass 📖	mathematical	—	upperCentralSeries Group.nilpotencyClass Top.top Subgroup Subgroup.instTop	—	Nat.find_spec Group.IsNilpotent.nilpotent
upperCentralSeries_one 📖	mathematical	—	upperCentralSeries Subgroup.center	—	Subgroup.ext mul_inv_eq_one mul_inv_eq_iff_eq_mul
upperCentralSeries_zero 📖	mathematical	—	upperCentralSeries Bot.bot Subgroup Subgroup.instBot	—	—

lowerCentralSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	—	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.map lowerCentralSeries	—	Subgroup.closure_induction Subgroup.mem_closure Subgroup.mem_map_of_mem map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv MonoidHom.map_one Subgroup.one_mem Subgroup.mul_mem MonoidHom.map_inv Subgroup.inv_mem

upperCentralSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	Subgroup Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder Subgroup.map upperCentralSeries	—	Subgroup.map_bot map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv Subgroup.mem_map_of_mem

---

← Back to Index