Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-04 22:27 1c4b5ec9

View on Github →

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

Estimated changes