isNilpotent_sub — Mathlib

English

If x and y commute in a ring and both are nilpotent, then their difference x − y is nilpotent.

Русский

Пусть x и y коммутируют в кольце и оба нилпотентны; тогда x − y также нилпотентен.

LaTeX

$$$ (Commute\\ x\\ y) \\Rightarrow \\bigl( IsNilpotent(x) \\to IsNilpotent(y) \\to IsNilpotent(x - y) \\bigr) $$$

Lean4

theorem isNilpotent_sub (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) : IsNilpotent (x - y) :=
  by
  rw [← neg_right_iff] at h_comm
  rw [← isNilpotent_neg_iff] at hy
  rw [sub_eq_add_neg]
  exact h_comm.isNilpotent_add hx hy

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