Def AddValuation.valuation

Modification history

2024-12-16 15:39

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory/Valuation/Basic): API for conversion `AddValuation` ↔ `Valuation` (#18786)

Deleted AddValuation.valuation View on Github →

2023-03-17 12:44

Mathlib/RingTheory/Valuation/Basic.lean

feat: port RingTheory.Valuation.Basic (#2846)

Added AddValuation.valuation View on Github →