Structures · Algebra
AddGroup.IsNilpotent
An additive 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 by32
- AddGroup.nilpotencyClass_def
- AddSubgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
- AddGroup.IsNilpotent.nilpotent
- AddSubgroup.lowerCentralSeries_length_eq_nilpotencyClass
- AddSubgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le
- AddSubgroup.lowerCentralSeries_nilpotencyClass
- AddGroup.nilpotencyClass_zero_iff_subsingleton
- AddSubgroup.upperCentralSeries_nilpotencyClass
- AddGroup.nilpotent_of_surjective
- AddSubgroup.least_descending_central_series_length_eq_nilpotencyClass
- AddGroup.IsNilpotent.nilpotent'
- AddGroup.nilpotencyClass_le_of_ker_le_center
- AddGroup.nilpotencyClass_le_of_surjective
- AddSubgroup.least_ascending_central_series_length_eq_nilpotencyClass
- AddSubgroup.isNilpotent_of_ker_le_center
- AddSubgroup.upperCentralSeries.eq_top
- AddGroup.nilpotent_quotient_of_nilpotent
- addCommGroupOfNilpotencyClass
- AddSubgroup.nilpotencyClass_le
- AddGroup.nilpotent_center_quotient_ind
- AddGroup.isNilpotent_pi
- AddGroup.nilpotencyClass_sum
- AddGroup.isNilpotent_pi_of_bounded_class
- AddGroup.isNilpotent_sum
- AddGroup.nilpotencyClass_pi
- AddGroup.nilpotent_of_addEquiv
- AddGroup.IsNilpotent.center_ne_bot
- AddGroup.IsNilpotent.nilpotencyClass_nonpos_iff
- AddGroup.nilpotencyClass_eq_quotient_center_plus_zero
- AddSubgroup.lowerCentralSeries_eq_bot_of_nilpotencyClass_le
- AddSubgroup.isNilpotent
- AddGroup.nilpotencyClass_quotient_le
Ancestors0
No ancestors.