isUnit_or_isUnit_one_sub_self — Mathlib

English

In a local ring R, for every a ∈ R, either a is a unit or 1 − a is a unit.

Русский

В локальном кольце R для каждого элемента a ∈ R либо a является единицей, либо 1 − a является единицей.

LaTeX

$$$[\\text{IsLocalRing } R]\\;\\Rightarrow\\; \\forall a\\in R,\\ IsUnit(a) \\lor IsUnit(1-a)$$$

Lean4

theorem isUnit_or_isUnit_one_sub_self (a : R) : IsUnit a ∨ IsUnit (1 - a) :=
  isUnit_or_isUnit_of_isUnit_add <| (add_sub_cancel a 1).symm ▸ isUnit_one

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