Def Valuation.congr

Modification history

2025-01-24 22:55
Mathlib/RingTheory/Valuation/Basic.lean
refactor: make `LinearOrderedCommMonoidWithZero` extend `OrderBot` (#19193) …
Added Valuation.congrView on Github →