Mathlib Changelog
v4
Changelog
About
Github
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 →