Commit 2026-03-02 13:09 a237616f

View on Github →

feat(Algebra/Homology): more lemmas for the biproduct of complexes (#35934)

Estimated changes

Modified Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean

added theorem HomologicalComplex.biprodX_ext_from

added theorem HomologicalComplex.biprodX_ext_from_iff

added theorem HomologicalComplex.biprodX_ext_to

added theorem HomologicalComplex.biprodX_ext_to_iff

added theorem HomologicalComplex.biprod_total_f