Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-06 23:05
4a435b5c
View on Github →
chore(CategoryTheory/ConcreteCategory): remove use of
erw
(
#32519
)
Estimated changes
Modified
Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean