Maximal ideal of local rings

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

Main definitions

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

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

The ideal of elements that are not units.

Equations

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

@[deprecated IsLocalRing.maximalIdeal (since := "2024-11-11")]

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

Alias of IsLocalRing.maximalIdeal.

---

The ideal of elements that are not units.

Equations

• LocalRing.maximalIdeal = IsLocalRing.maximalIdeal