Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-18 09:18
071d4f73
View on Github →
Merge remote-tracking branch 'origin/shift_induced'
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Shift/Induced.lean
added
def
CategoryTheory.Functor.CommShift.ofInduced
added
theorem
CategoryTheory.Functor.commShiftIso_eq_ofInduced
added
theorem
CategoryTheory.HasShift.Induced.add_hom_app_obj
added
theorem
CategoryTheory.HasShift.Induced.add_inv_app_obj
added
theorem
CategoryTheory.HasShift.Induced.zero_hom_app_obj
added
theorem
CategoryTheory.HasShift.Induced.zero_inv_app_obj
added
theorem
CategoryTheory.induced_add_inv_app_obj
added
theorem
CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced
added
theorem
CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced
added
theorem
CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced
added
theorem
CategoryTheory.shiftFunctor_of_induced