isUnit_or_isUnit_of_isUnit_add — Mathlib

English

In a local ring, the sum of two nonunits cannot be a unit.

Русский

В локальном кольце сумма двух неприводимых не может быть единицей.

LaTeX

$$$$\text{In a local ring } a,b \notin \text{nonunits} \Rightarrow a+b \notin \text{units}. $$$$

Lean4

theorem isUnit_or_isUnit_of_isUnit_add {a b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b :=
  by
  rcases h with ⟨u, hu⟩
  rw [← Units.inv_mul_eq_one, mul_add] at hu
  apply Or.imp _ _ (isUnit_or_isUnit_of_add_one hu) <;> exact isUnit_of_mul_isUnit_right

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