Def Valuation.RankOne.ofRankLeOneStruct

Modification history

2025-07-08 21:40

Mathlib/RingTheory/Valuation/RankOne.lean

feat(Valuation/RankOne): equivalence with ValuativeRel.isRankLeOne (#26754) …

Added Valuation.RankOne.ofRankLeOneStruct View on Github →