Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 20:37 119eb05e

View on Github →

chore(ring_theory/valuation/basic): fix valuation_apply (#13045) Follow-up to #12914.

Estimated changes