Commit 2023-08-18 09:39 268a8e25

View on Github →

trying to revert unwanted commits

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/CategoryTheory/Shift/Induced.lean

deleted def CategoryTheory.Functor.CommShift.ofInduced

deleted theorem CategoryTheory.Functor.commShiftIso_eq_ofInduced

deleted theorem CategoryTheory.HasShift.Induced.add_hom_app_obj

deleted theorem CategoryTheory.HasShift.Induced.add_inv_app_obj

deleted theorem CategoryTheory.HasShift.Induced.zero_hom_app_obj

deleted theorem CategoryTheory.HasShift.Induced.zero_inv_app_obj

deleted theorem CategoryTheory.induced_add_inv_app_obj

deleted theorem CategoryTheory.shiftFunctorAdd_hom_app_obj_of_induced

deleted theorem CategoryTheory.shiftFunctorZero_hom_app_obj_of_induced

deleted theorem CategoryTheory.shiftFunctorZero_inv_app_obj_of_induced

deleted theorem CategoryTheory.shiftFunctor_of_induced

Deleted Mathlib/CategoryTheory/Shift/Quotient.lean

deleted theorem CategoryTheory.HasShift.quotient'_aux

deleted def CategoryTheory.Quotient.shiftFunctor'

deleted def CategoryTheory.Quotient.shiftFunctor'Factors