Commit 2024-06-24 07:53 aaafbd98

View on Github →

feat: the extension of a homological complex by an embedding of complex shapes (#13992)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/Embedding/Basic.lean

added theorem ComplexShape.Embedding.f_eq_of_r_eq_some

added theorem ComplexShape.Embedding.r_eq_none

added theorem ComplexShape.Embedding.r_eq_some

added theorem ComplexShape.Embedding.r_f

Created Mathlib/Algebra/Homology/Embedding/Extend.lean

added theorem HomologicalComplex.extend.d_eq

added theorem HomologicalComplex.extend.d_none_eq_zero'

added theorem HomologicalComplex.extend.d_none_eq_zero

added theorem HomologicalComplex.extend.isZero_X

added theorem HomologicalComplex.extend_d_eq

added theorem HomologicalComplex.extend_d_from_eq_zero

added theorem HomologicalComplex.extend_d_to_eq_zero

added theorem HomologicalComplex.isZero_extend_X'

added theorem HomologicalComplex.isZero_extend_X

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.eq_none_or_eq_some