# Local rings #

We prove basic properties of local rings.

source
theorem IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [Semiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) :
IsLocalRing R
source
theorem IsLocalRing.of_nonunits_add {R : Type u_1} [Semiring R] [Nontrivial R] (h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) :
IsLocalRing R

A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

source
theorem IsLocalRing.of_unique_max_ideal {R : Type u_1} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) :
IsLocalRing R

A semiring is local if it has a unique maximal ideal.

source
theorem IsLocalRing.of_unique_nonzero_prime {R : Type u_1} [CommSemiring R] (h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) :
IsLocalRing R
source
theorem IsLocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (h : IsUnit (a + b)) :
IsUnit a ∨ IsUnit b
source
theorem IsLocalRing.nonunits_add {R : Type u_1} [CommSemiring R] [IsLocalRing R] {a b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) :
a + b ∈ nonunits R
source
theorem IsLocalRing.of_isUnit_or_isUnit_one_sub_self {R : Type u_1} [Ring R] [Nontrivial R] (h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) :
IsLocalRing R
source
theorem IsLocalRing.isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) :
IsUnit a ∨ IsUnit (1 - a)
source
theorem IsLocalRing.isUnit_of_mem_nonunits_one_sub_self {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : 1 - a ∈ nonunits R) :
IsUnit a
source
theorem IsLocalRing.isUnit_one_sub_self_of_mem_nonunits {R : Type u_1} [CommRing R] [IsLocalRing R] (a : R) (h : a ∈ nonunits R) :
IsUnit (1 - a)
source
theorem IsLocalRing.of_surjective' {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [Ring S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective ⇑f) :
IsLocalRing S
source
@[instance 100]
instance Field.instIsLocalRing (K : Type u_3) [Field K] :
IsLocalRing K