Documentation

Mathlib.RingTheory.LocalRing.Defs

Local rings #

Define local rings as commutative rings having a unique maximal ideal.

Main definitions #

class LocalRing (R : Type u_1) [Semiring R] extends Nontrivial :

A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1. Note that LocalRing is a predicate.

  • of_is_unit_or_is_unit_of_add_one :: (
    • exists_pair_ne : ∃ (x : R), ∃ (y : R), x y
    • isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1IsUnit 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.

  • )
Instances
    theorem LocalRing.isUnit_or_isUnit_of_add_one {R : Type u_1} :
    ∀ {inst : Semiring R} [self : LocalRing R] {a b : R}, a + b = 1IsUnit 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.