Theorem AddValuation.ofValuation_symm_eq

Modification history

2024-12-16 15:39

Mathlib/RingTheory/Valuation/Basic.lean

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

Added AddValuation.ofValuation_symm_eq View on Github →