Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-06 18:41
c29699f0
View on Github →
chore(Algebra/Module/LinearMap): remove use of
erw
(
#32489
)
Estimated changes
Modified
Mathlib/Algebra/Module/LinearMap/Basic.lean