Maximal ideal of local rings

We define the maximal ideal of a local ring as the ideal of all non units.

Main definitions

• LocalRing.maximalIdeal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.

def LocalRing.maximalIdeal (R : Type u_1) [CommSemiring R] [LocalRing R] : Ideal R

The ideal of elements that are not units.

Equations

• LocalRing.maximalIdeal R = { carrier := nonunits R, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }