Theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered

Modification history

2025-07-11 08:42
Mathlib/RingTheory/Valuation/Archimedean.lean
chore(Valuation/Archimedean): generalize `isPrincipalIdealRing_iff_not_denselyOrdered` to only discuss mrange (#26943) …
Modified Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrderedView on Github →
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.isPrincipalIdealRing_iff_not_denselyOrderedView on Github →