Commit 2023-09-14 17:32 7c77a529

View on Github →

feat: the complex of homomorphisms between two cochain complexes (#7050)

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

added theorem CochainComplex.HomComplex.δ_add

added theorem CochainComplex.HomComplex.δ_comp

added theorem CochainComplex.HomComplex.δ_comp_zero_cochain

added def CochainComplex.HomComplex.δ_hom

added theorem CochainComplex.HomComplex.δ_neg

added theorem CochainComplex.HomComplex.δ_neg_one_cochain

added theorem CochainComplex.HomComplex.δ_ofHom

added theorem CochainComplex.HomComplex.δ_ofHomotopy

added theorem CochainComplex.HomComplex.δ_sub

added theorem CochainComplex.HomComplex.δ_zero

added theorem CochainComplex.HomComplex.δ_zero_cochain_comp

added theorem CochainComplex.HomComplex.δ_zero_cochain_v

added theorem CochainComplex.HomComplex.δ_zsmul

added theorem CochainComplex.HomComplex.δ_δ

added def CochainComplex.HomComplex