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.wfDvdMonoid_iff_wellFounded_gt_on_v