Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes