Commit 2023-11-04 08:45 7e0b41d4

View on Github →

feat: homology of chain complexes in degree 0 (#8169)

Estimated changes

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

added theorem ChainComplex.isoHomologyι₀_inv_naturality

added theorem CochainComplex.isoHomologyπ₀_inv_naturality

modified theorem HomologicalComplex.exactAt_iff_isZero_homology

added theorem HomologicalComplex.iCyclesIso_hom_inv_id

added theorem HomologicalComplex.iCyclesIso_inv_hom_id

added theorem HomologicalComplex.isIso_homologyι

added theorem HomologicalComplex.isIso_homologyπ

added theorem HomologicalComplex.isIso_iCycles

added theorem HomologicalComplex.isIso_pOpcycles

added theorem HomologicalComplex.isoHomologyι_hom_inv_id

added theorem HomologicalComplex.isoHomologyι_inv_hom_id

added theorem HomologicalComplex.isoHomologyπ_hom_inv_id

added theorem HomologicalComplex.isoHomologyπ_inv_hom_id

added theorem HomologicalComplex.pOpcyclesIso_hom_inv_id

added theorem HomologicalComplex.pOpcyclesIso_inv_hom_id