Commit 2023-11-01 07:43 d1889482

View on Github →

feat: more API for homotopies of short complexes (#8069)

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

added def CategoryTheory.ShortComplex.Homotopy.add

added def CategoryTheory.ShortComplex.Homotopy.comp

added def CategoryTheory.ShortComplex.Homotopy.compLeft

added def CategoryTheory.ShortComplex.Homotopy.compRight

added theorem CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic

added def CategoryTheory.ShortComplex.Homotopy.equivSubZero

added def CategoryTheory.ShortComplex.Homotopy.neg

added def CategoryTheory.ShortComplex.Homotopy.ofEq

added def CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic

added def CategoryTheory.ShortComplex.Homotopy.op

added def CategoryTheory.ShortComplex.Homotopy.refl

added def CategoryTheory.ShortComplex.Homotopy.sub

added def CategoryTheory.ShortComplex.Homotopy.symm

added def CategoryTheory.ShortComplex.Homotopy.trans

added def CategoryTheory.ShortComplex.Homotopy.unop

added def CategoryTheory.ShortComplex.nullHomotopic