of_isUnit_or_isUnit_one_sub_self — Mathlib

English

Let R be a nontrivial ring. If for every a ∈ R, either a is a unit or 1 − a is a unit, then R is a local ring.

Русский

Пусть R — ненулевое кольцо. Если для каждого a ∈ R выполняется, что либо a является единицей, либо 1 − a является единицей, тогда R является локальным кольцом.

LaTeX

$$$R\\quad\\text{is a nontrivial ring and }\\forall a\\in R,\\ (a \\in R^{\\times}) \\lor ((1-a) \\in R^{\\times})\\ \\Rightarrow\\ R \\text{ is local}$$$

Lean4

theorem of_isUnit_or_isUnit_one_sub_self [Nontrivial R] (h : ∀ a : R, IsUnit a ∨ IsUnit (1 - a)) : IsLocalRing R :=
  ⟨fun {a b} hab => add_sub_cancel_left a b ▸ hab.symm ▸ h a⟩

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