feat(ring_theory/ideals): quotient map to residue field as ring hom (#2597)

Author: jcommelin

src/ring_theory/ideals.lean

@@ -479,11 +479,15 @@ variables [local_ring α] [local_ring β]
 variable (α)
 def residue_field := (nonunits_ideal α).quotient
 
-namespace residue_field
-
-noncomputable instance : field (residue_field α) :=
+noncomputable instance residue_field.field : field (residue_field α) :=
 ideal.quotient.field (nonunits_ideal α)
 
+/-- The quotient map from a local ring to it's residue field. -/
+def residue : α →+* (residue_field α) :=
+ideal.quotient.mk_hom _
+
+namespace residue_field
+
 variables {α β}
 noncomputable def map (f : α →+* β) [is_local_ring_hom f] :
   residue_field α →+* residue_field β :=