Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-17 11:16
485b736d
View on Github →
refactor(Algebra/Lie/BaseChange): use new tensor product machinery (
#6628
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Lie/BaseChange.lean
modified
theorem
LieAlgebra.ExtendScalars.bracket_tmul
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
Modified
Mathlib/Init/Data/Nat/Lemmas.lean
Modified
lake-manifest.json