isNilpotent — Mathlib

English

The nilpotency class of a subgroup is less than or equal to that of the ambient group.

Русский

Класс нильпотентности подгруппы не превосходит класса группы.

LaTeX

$$Group.nilpotencyClass H \\le Group.nilpotencyClass G$$

Lean4

/-- A subgroup of a nilpotent group is nilpotent -/
instance isNilpotent (H : Subgroup G) [hG : IsNilpotent G] : IsNilpotent H :=
  by
  rw [nilpotent_iff_lowerCentralSeries] at *
  rcases hG with ⟨n, hG⟩
  use n
  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⟩)

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