Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-23 15:20 270fc310

View on Github →

fix(ring_theory/discrete_valuation_ring): docstring typos (#5085) Clarify one docstring and fix two others.

Estimated changes