Local rings

Define the notion of a local ring for non-commutative semirings. In the commutative case, this is shown to be equivalent to the familiar definition that there exists a unique maximal ideal in IsLocalRing.of_unique_max_ideal and IsLocalRing.maximal_ideal_unique.

Main definitions

• IsLocalRing: A predicate on semirings, stating that for any pair of elements that adds up to 1, one of them is a unit.

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

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

• of_is_unit_or_is_unit_of_add_one :: (
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one {a b : R} (h : 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.

• )