of_isUnit_or_isUnit_of_isUnit_add

English

In a local ring, if a + b is a unit, then either a or b is a unit.

Русский

В локальном кольце, если a + b — единица, то либо a, либо b — единица.

LaTeX

$$$$\text{If } a+b \text{ is a unit, then } a \text{ is a unit or } b \text{ is a unit.}$$$$

Lean4

theorem of_isUnit_or_isUnit_of_isUnit_add [Nontrivial R] (h : ∀ a b : R, IsUnit (a + b) → IsUnit a ∨ IsUnit b) :
    IsLocalRing R :=
  ⟨fun {a b} hab => h a b <| hab.symm ▸ isUnit_one⟩

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