Commit 2025-07-11 08:42 d79bad3a

View on Github →

chore(Valuation/Archimedean): generalize isPrincipalIdealRing_iff_not_denselyOrdered to only discuss mrange (#26943) This is stronger, because the codomain could be not mul-archimedean Could help with #26623

Estimated changes

Modified Mathlib/RingTheory/Valuation/Archimedean.lean

modified theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered

Modified Mathlib/Topology/Algebra/Valued/LocallyCompact.lean

modified theorem Valued.integer.isPrincipalIdealRing_of_compactSpace