nilpotencyClass_le — Mathlib

English

A subgroup of a nilpotent group is nilpotent.

Русский

Подгруппа нильпотентной группы также нильпотентна.

LaTeX

$$$IsNilpotent(H)\\;\\text{given } IsNilpotent(G)$$$

Lean4

/-- The nilpotency class of a subgroup is less or equal to the nilpotency class of the group -/
theorem nilpotencyClass_le (H : Subgroup G) [hG : IsNilpotent G] : Group.nilpotencyClass H ≤ Group.nilpotencyClass G :=
  by
  repeat rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  classical apply Nat.find_mono
  intro n hG
  have := lowerCentralSeries_map_subtype_le H n
  simp only [hG, SetLike.le_def, mem_map, exists_imp] at this
  exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)

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