Maximal ideal of local rings

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

Main definitions

• IsLocalRing.maximalIdeal: The unique maximal ideal for a local rings. Its carrier set is the set of nonunits.

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

The ideal of elements that are not units.