Residue Field of local rings

Main definitions

• IsLocalRing.ResidueField: The quotient of a local ring by its maximal ideal.
• IsLocalRing.residue: The quotient map from a local ring to its residue field.

def IsLocalRing.ResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] : Type u_1

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

@[implicit_reducible]

instance IsLocalRing.instCommRingResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] : CommRing (ResidueField R)

@[implicit_reducible]

instance IsLocalRing.instInhabitedResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] : Inhabited (ResidueField R)

@[implicit_reducible]

noncomputable instance IsLocalRing.ResidueField.field (R : Type u_1) [CommRing R] [IsLocalRing R] : Field (ResidueField R)

def IsLocalRing.residue (R : Type u_1) [CommRing R] [IsLocalRing R] : R →+* ResidueField R

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