Mathlib Changelog
Changelog
About
Github
Commit
2021-12-22 21:32
c5bb320c
View on Github →
refactor(*): Random lemmas and modifications from the shifting refactor. (
#10940
)
Estimated changes
Modified
src/algebra/homology/differential_object.lean
added
def
category_theory.differential_object.X_eq_to_hom
added
theorem
category_theory.differential_object.X_eq_to_hom_refl
added
theorem
homological_complex.d_eq_to_hom
added
theorem
homological_complex.eq_to_hom_d
added
theorem
homological_complex.eq_to_hom_f
Modified
src/category_theory/differential_object.lean
added
theorem
category_theory.differential_object.eq_to_hom_f
added
def
category_theory.differential_object.mk_iso
Modified
src/category_theory/equivalence.lean
added
theorem
category_theory.functor.as_equivalence_counit
added
theorem
category_theory.functor.as_equivalence_unit
Modified
src/category_theory/graded_object.lean
added
theorem
category_theory.graded_object.eq_to_hom_apply
Modified
src/category_theory/limits/has_limits.lean
added
theorem
category_theory.limits.has_smallest_colimits_of_has_colimits
added
theorem
category_theory.limits.has_smallest_limits_of_has_limits
Modified
src/category_theory/monoidal/End.lean
added
theorem
category_theory.μ_inv_naturalityᵣ
added
theorem
category_theory.μ_inv_naturalityₗ
Modified
src/category_theory/monoidal/discrete.lean
Modified
src/category_theory/natural_isomorphism.lean
Modified
src/category_theory/triangulated/basic.lean
modified
def
category_theory.triangulated.triangle.mk