Theorem CategoryTheory.SmallObject.functorMap_π

Modification history

2025-02-03 19:15
Mathlib/CategoryTheory/SmallObject/Construction.lean
feat(CategoryTheory/SmallObject): promote a construction from `Over` to `Arrow` (#20260) …
Modified CategoryTheory.SmallObject.functorMap_πView on Github →
2024-03-18 20:42
Mathlib/CategoryTheory/SmallObject/Construction.lean
feat(CategoryTheory): construction of a functor for the small object argument (#11056) …
Added CategoryTheory.SmallObject.functorMap_πView on Github →