Theorems · Theorem · commutative algebra

IsLocalRing.isUnit_or_isUnit_of_add_one

∀ {R : Type u_1} {inst : Semiring R} [self : IsLocalRing R] {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b

in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.

Defined in

Mathlib.RingTheory.LocalRing.Defs

Cited by

5 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

IsLocalRing