feat(ring_theory/ideal/local_ring): residue field is an algebra (#8991)
feat(ring_theory/ideal/local_ring): residue field is an algebra (#8991)

Also, the kernel of a surjective map to a field is equal to the unique maximal ideal.








leanprover-community/mathlib,leanprover-community/mathlib