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.
The residue field of a local ring is the quotient of the ring by its maximal ideal.
Equations
Instances For
instance
IsLocalRing.ResidueFieldCommRing
(R : Type u_1)
[CommRing R]
[IsLocalRing R]
:
CommRing (ResidueField R)
Equations
Equations
noncomputable instance
IsLocalRing.ResidueField.field
(R : Type u_1)
[CommRing R]
[IsLocalRing R]
:
Field (ResidueField R)
The quotient map from a local ring to its residue field.
Equations
Instances For
@[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.
Instances For
@[deprecated IsLocalRing.residue (since := "2024-11-11")]
Alias of IsLocalRing.residue
.
The quotient map from a local ring to its residue field.