Mathlib Changelog
v4
Changelog
About
Github
Theorem
Valuation.ofAddValuation_toAddValuation
Modification history
2025-07-25 22:49
Mathlib/RingTheory/Valuation/Basic.lean
chore: fix more indentation (#27494) …
Modified
Valuation.ofAddValuation_toAddValuation
View on Github →
2024-12-16 15:39
Mathlib/RingTheory/Valuation/Basic.lean
feat(RingTheory/Valuation/Basic): API for conversion `AddValuation` ↔ `Valuation` (#18786)
Added
Valuation.ofAddValuation_toAddValuation
View on Github →