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
Instances For

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

    Equations
    Instances For