of_nonunits_add — Mathlib

English

A semiring with a unique maximal ideal is local.

Русский

Полукольцо с единственным максимальным идеалом есть локальное.

LaTeX

$$$$\text{If } R \text{ has a unique maximal ideal, then } R \text{ is local.}$$$$

Lean4

/-- A semiring is local if it is nontrivial and the set of nonunits is closed under the addition. -/
theorem of_nonunits_add [Nontrivial R] (h : ∀ a b : R, a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) :
    IsLocalRing R where
  isUnit_or_isUnit_of_add_one {a b} hab := or_iff_not_and_not.2 fun H => h a b H.1 H.2 <| hab.symm ▸ isUnit_one

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