Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-20 14:26
aa8d81bf
View on Github →
feat(CategoryTheory/Elements): taking a functor to its category of elements is functorial (
#15784
)
Estimated changes
Modified
Mathlib/CategoryTheory/Elements.lean
added
def
CategoryTheory.Functor.elementsFunctor
added
def
CategoryTheory.NatTrans.mapElements