Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-10 19:57
4422acf8
View on Github →
fix: add deprecation alias (
#13693
) This PR adds a deprecation alias that was missing from
#10088
.
Estimated changes
Modified
Mathlib/RingTheory/IntegralDomain.lean