Commit 2021-09-07 11:06 d69c12e9
View on Github →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.
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.