Theorem AddValuation.toValuation_apply

Modification history

2024-12-16 15:39
Mathlib/RingTheory/Valuation/Basic.lean
feat(RingTheory/Valuation/Basic): API for conversion `AddValuation` ↔ `Valuation` (#18786)
Added AddValuation.toValuation_applyView on Github →