Commit 2023-04-18 11:12 8efb2cb1

View on Github →

feat: port Algebra.Homology.Single (#3495)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/Single.lean

added def ChainComplex.fromSingle₀Equiv

added def ChainComplex.single₀

added def ChainComplex.single₀IsoSingle

added theorem ChainComplex.single₀_map_f_0

added theorem ChainComplex.single₀_map_f_succ

added theorem ChainComplex.single₀_obj_X_0

added theorem ChainComplex.single₀_obj_X_d

added theorem ChainComplex.single₀_obj_X_dTo

added theorem ChainComplex.single₀_obj_X_succ

added theorem ChainComplex.single₀_obj_x_dFrom

added def ChainComplex.toSingle₀Equiv

added theorem ChainComplex.to_single₀_ext

added def CochainComplex.fromSingle₀Equiv

added theorem CochainComplex.from_single₀_ext

added def CochainComplex.single₀

added def CochainComplex.single₀IsoSingle

added theorem CochainComplex.single₀_map_f_0

added theorem CochainComplex.single₀_map_f_succ

added theorem CochainComplex.single₀_obj_X_0

added theorem CochainComplex.single₀_obj_X_d

added theorem CochainComplex.single₀_obj_X_succ

added theorem CochainComplex.single₀_obj_x_dFrom

added theorem CochainComplex.single₀_obj_x_dTo

added def HomologicalComplex.single

added def HomologicalComplex.singleObjXSelf

added theorem HomologicalComplex.single_map_f_self