lowerCentralSeries_succ_eq_bot — Mathlib

English

If γ_n(G) ≤ Z(G), then γ_{n+1}(G) = ⊥.

Русский

Если γ_n(G) ≤ Z(G), то γ_{n+1}(G) = ⊥.

LaTeX

$$lowerCentralSeries G (n+1) = ⊥ \\text{ if } lowerCentralSeries G n \\le center G$$

Lean4

theorem lowerCentralSeries_succ_eq_bot {n : ℕ} (h : lowerCentralSeries G n ≤ center G) :
    lowerCentralSeries G (n + 1) = ⊥ :=
  by
  rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]
  rintro x ⟨y, hy1, z, ⟨⟩, rfl⟩
  rw [mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]
  exact mem_center_iff.mp (h hy1) z

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