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