Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-28 15:02
31f931fe
View on Github →
feat(RingTheory/DedekindDomain/AdicValuation): add eq_of_valuation_isEquiv_valuation (
#30404
)
Estimated changes
Modified
Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
added
theorem
IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation