Theorem ValuativeRel.isNontrivial_of_rankOne

Modification history

2025-07-08 21:40
Mathlib/RingTheory/Valuation/RankOne.lean
feat(Valuation/RankOne): equivalence with ValuativeRel.isRankLeOne (#26754) …
Added ValuativeRel.isNontrivial_of_rankOneView on Github →