Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-17 15:45
f7cf7edc
View on Github →
pleasing the linter
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
Modified
Mathlib/Init/Data/Nat/Lemmas.lean
Modified
lake-manifest.json