isUnit_add_right_of_commute — Mathlib

English

If r is nilpotent, u is a unit, and r commutes with u, then r + u is a unit.

Русский

Если r нильпотентен, u — единица, и r коммутиирует с u, то r + u — единица.

LaTeX

$$$ \\text{IsNilpotent}(r) \\rightarrow \\text{IsUnit}(u) \\rightarrow \\text{Commute}(r,u) \\rightarrow \\text{IsUnit}(r + u) $$$

Lean4

theorem isUnit_add_right_of_commute [Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (r + u) :=
  add_comm r u ▸ hnil.isUnit_add_left_of_commute hu h_comm

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