nilpotencyClass_eq_quotient_center_plus_one

English

If G is nilpotent and nontrivial, then the nilpotency class of G equals the nilpotency class of G/Z(G) plus 1.

Русский

Если G нильпотентна и не тривиальна, то класс нильпотентности G равен классу G/Z(G) плюс 1.

LaTeX

$$$\\operatorname{nilpotencyClass}(G) = \\operatorname{nilpotencyClass}(G/Z(G)) + 1$$$

Lean4

/-- The nilpotency class of a non-trivial group is one more than its quotient by the center -/
theorem nilpotencyClass_eq_quotient_center_plus_one [hH : IsNilpotent G] [Nontrivial G] :
    Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ center G) + 1 :=
  by
  rw [nilpotencyClass_quotient_center]
  rcases h : Group.nilpotencyClass G with ⟨⟩
  · exfalso
    rw [nilpotencyClass_zero_iff_subsingleton] at h
    apply false_of_nontrivial_of_subsingleton G
  · simp

Похожие утверждения