Theorems · Theorem · group theory
AddGroup.nilpotencyClass_eq_quotient_center_plus_zero
∀ {G : Type u_1} [inst : AddGroup G] [hH : AddGroup.IsNilpotent G] [Nontrivial G],
AddGroup.nilpotencyClass G = AddGroup.nilpotencyClass (G ⧸ AddSubgroup.center G) + 1The nilpotency class of a non-trivial additive group is one more than its quotient by the center
- Defined in
- Mathlib.GroupTheory.Nilpotent
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- Nontrivialstatement and proof · cited by 2,416
- HasQuotient.Quotientstatement · cited by 2,301
- add_tsub_cancel_rightproof · cited by 172
- AddGroup.IsNilpotentstatement and proof · cited by 42
- AddSubgroup.centerstatement · cited by 40
- AddGroup.nilpotencyClassstatement and proof · cited by 26
- false_of_nontrivial_of_subsingletonproof · cited by 5
- AddGroup.nilpotencyClass_quotient_centerproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.