Structures · Algebra
Group.IsNilpotent
A group G is nilpotent if its upper central series is eventually G.
- Defined in
- Mathlib.GroupTheory.Nilpotent
- Shape
- One type argument · adds nilpotent'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Subtype
- Prod
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by64
- Subgroup.lowerCentralSeries_length_eq_nilpotencyClass
- Group.nilpotencyClass_def
- Group.IsNilpotent.nilpotent
- Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le
- Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
- Subgroup.lowerCentralSeries_nilpotencyClass
- Group.nilpotent_of_surjective
- Subgroup.upperCentralSeries_nilpotencyClass
- Subgroup.least_ascending_central_series_length_eq_nilpotencyClass
- Subgroup.least_descending_central_series_length_eq_nilpotencyClass
- Group.nilpotencyClass_zero_iff_subsingleton
- Group.nilpotent_of_mulEquiv
- Group.nilpotencyClass_le_of_ker_le_center
- Group.normalizerCondition_of_isNilpotent
- Subgroup.upperCentralSeries.eq_top
- Group.nilpotencyClass_le_of_surjective
- Subgroup.isNilpotent_of_ker_le_center
- Group.nilpotent_center_quotient_ind
- Group.IsNilpotent.nilpotent'
- Group.nilpotencyClass_eq_quotient_center_plus_one
- Group.nilpotencyClass_prod
- Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent
- Group.nilpotencyClass_pi
- Group.isNilpotent_pi_of_bounded_class
- Group.nilpotencyClass_quotient_le
- IsNilpotent.to_isSolvable
- nilpotent_of_surjective
- commGroupOfNilpotencyClass
- isNilpotent_pi_of_bounded_class
- IsZGroup.instIsCyclicOfFiniteOfIsNilpotent
- lowerCentralSeries_nilpotencyClass
- least_descending_central_series_length_eq_nilpotencyClass
- nilpotencyClass_eq_quotient_center_plus_one
- nilpotent_quotient_of_nilpotent
- nilpotencyClass_le_one_of_isSimple_of_isNilpotent
- instNormalOfIsNilpotentOfFactPrime
- nilpotencyClass_quotient_le
- Subgroup.lowerCentralSeries_eq_bot_of_nilpotencyClass_le
- isNilpotent_prod
- Group.isNilpotent_pi
- upperCentralSeries_eq_top_iff_nilpotencyClass_le
- lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
- isNilpotent_of_ker_le_center
- upperCentralSeries.eq_top
- nilpotencyClass_prod
- nilpotencyClass_le_of_surjective
- nilpotencyClass_zero_iff_subsingleton
- normalizerCondition_of_isNilpotent
- nilpotent_center_quotient_ind
- upperCentralSeries_nilpotencyClass
Ancestors0
No ancestors.