isUnit_add_left_of_commute — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isUnit_add_left_of_commute [Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (u + r) := by
  rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]
  replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm
  refine IsNilpotent.isUnit_one_add ?_
  exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

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