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