isNilpotent_add — Mathlib

English

If x and y are nilpotent and commute, then x+y is nilpotent.

Русский

Если x и y нильпотентны и коммутируют, то x+y нильпотентен.

LaTeX

$$$\\text{Commute}(x,y) \\land \\text{IsNilpotent}(x) \\land \\text{IsNilpotent}(y) \\Rightarrow \\text{IsNilpotent}(x+y)$$$

Lean4

theorem isNilpotent_add (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent (x + y) :=
  by
  obtain ⟨n, hn⟩ := hx
  obtain ⟨m, hm⟩ := hy
  exact ⟨_, add_pow_add_eq_zero_of_pow_eq_zero h_comm hn hm⟩

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