Theorem CategoryTheory.shiftFunctorAdd_inv_app_obj_of_induced

Modification history

2023-09-04 15:04
Mathlib/CategoryTheory/Shift/Induced.lean
feat: the induced shift on the target category of a functor (#6652) …
Added CategoryTheory.shiftFunctorAdd_inv_app_obj_of_inducedView on Github →