Theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange

Modification history

2025-09-23 17:30
Mathlib/RingTheory/Valuation/Archimedean.lean
chore: clean up some proofs about locally compact valuation (#28669)
Added Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrangeView on Github →