Theorem AddValuation.valuation_apply

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_applyView on Github →
2023-03-17 12:44
Mathlib/RingTheory/Valuation/Basic.lean
feat: port RingTheory.Valuation.Basic (#2846)
Added AddValuation.valuation_applyView on Github →