mathlib

1e9f6646 - refactor(ring_theory/discrete_valuation_ring): `discrete_valuation_ring.add_val` as an `add_valuation` (#6660)

refactor(ring_theory/discrete_valuation_ring): `discrete_valuation_ring.add_val` as an `add_valuation` (#6660) Refactors `discrete_valuation_ring.add_val` to be an `enat`-valued `add_valuation`. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>