Commit 2024-12-16 15:39 625ac34a

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

added def AddValuation.ofValuation

added theorem AddValuation.ofValuation_apply

added theorem AddValuation.ofValuation_symm_eq

added theorem AddValuation.ofValuation_toValuation

added def AddValuation.toValuation

added theorem AddValuation.toValuation_apply

added theorem AddValuation.toValuation_ofValuation

added theorem AddValuation.toValuation_symm_eq

deleted def AddValuation.valuation

deleted theorem AddValuation.valuation_apply

added def Valuation.ofAddValuation

added theorem Valuation.ofAddValuation_apply

added theorem Valuation.ofAddValuation_symm_eq

added theorem Valuation.ofAddValuation_toAddValuation

added def Valuation.toAddValuation

added theorem Valuation.toAddValuation_apply

added theorem Valuation.toAddValuation_symm_eq

added theorem Valuation.toValuation_ofValuation