Commit 2024-02-13 21:51 69334742

View on Github →

feat(Algebra/Homology): the total complex of a bicomplex (#9331)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/TotalComplex.lean

added theorem HomologicalComplex₂.D₁_D₁

added theorem HomologicalComplex₂.D₁_D₂

added theorem HomologicalComplex₂.D₁_shape

added theorem HomologicalComplex₂.D₂_D₁

added theorem HomologicalComplex₂.D₂_D₂

added theorem HomologicalComplex₂.D₂_shape

added theorem HomologicalComplex₂.d₁_eq'

added theorem HomologicalComplex₂.d₁_eq

added theorem HomologicalComplex₂.d₁_eq_zero'

added theorem HomologicalComplex₂.d₁_eq_zero

added theorem HomologicalComplex₂.d₂_eq'

added theorem HomologicalComplex₂.d₂_eq

added theorem HomologicalComplex₂.d₂_eq_zero'

added theorem HomologicalComplex₂.d₂_eq_zero

added theorem HomologicalComplex₂.ι_D₁

added theorem HomologicalComplex₂.ι_D₂

Modified Mathlib/CategoryTheory/GradedObject.lean

added theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq

added theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero