Commit 2025-09-23 17:30 4e6270f8

View on Github →

chore: clean up some proofs about locally compact valuation (#28669)

Estimated changes

Modified Mathlib/RingTheory/Valuation/Archimedean.lean

added theorem Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered_mrange

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.isNontrivial_iff_exists_lt_one

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

added theorem Valuation.isNontrivial_iff_not_a_field