Theorem Valuation.isNontrivial_iff_exists_lt_one

Modification history

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