Theorem ValuativeRel.IsNontrivial.exists_lt_one

Modification history

2025-11-20 14:55
Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
feat(Valuation): uniformizer of discrete valuation (#30259)
Added ValuativeRel.IsNontrivial.exists_lt_oneView on Github →