isUnit_one_sub_self_of_mem_nonunits

English

In a local ring R, if a ∈ nonunits, then 1 − a is a unit.

Русский

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

LaTeX

$$$[\\text{IsLocalRing } R]\\;\\text{ and } a\\in \\text{ nonunits }(R) \\Rightarrow IsUnit(1-a)$$$

Lean4

theorem isUnit_one_sub_self_of_mem_nonunits (a : R) (h : a ∈ nonunits R) : IsUnit (1 - a) :=
  or_iff_not_imp_left.1 (isUnit_or_isUnit_one_sub_self a) h

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