Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Defs

Residue Field of local rings #

Main definitions #

The residue field of a local ring is the quotient of the ring by its maximal ideal.

Equations

The quotient map from a local ring to its residue field.

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

Alias of IsLocalRing.ResidueField.


The residue field of a local ring is the quotient of the ring by its maximal ideal.

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

Alias of IsLocalRing.residue.


The quotient map from a local ring to its residue field.

Equations