local_ring): residue field is an algebra (#8991)

Commit

4 years ago

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.

Author

jcommelin

Parents

58a88539

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

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