2025-01-14 16:01
Mathlib/RingTheory/Valuation/Archimedean.lean
feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered (#16619)
Added Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange