Theorem Valuation.isNontrivial_iff_not_a_field

Modification history

2025-09-23 17:30
Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
chore: clean up some proofs about locally compact valuation (#28669)
Added Valuation.isNontrivial_iff_not_a_fieldView on Github →