Def CategoryTheory.NatTrans.mapElements

Modification history

2026-09-03 15:14
Mathlib/CategoryTheory/Elements.lean
refactor(CategoryTheory): cleaning up `Functor.Elements` (#43228) …
Modified CategoryTheory.NatTrans.mapElementsView on Github →
2024-08-20 14:26
Mathlib/CategoryTheory/Elements.lean
feat(CategoryTheory/Elements): taking a functor to its category of elements is functorial (#15784)
Added CategoryTheory.NatTrans.mapElementsView on Github →