Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-08 09:28 41e8eb32

View on Github →

feat(ring_theory/localization): quotient ring of integral domain is discrete field

Estimated changes