Mathlib Changelog
Changelog
About
Github
Commit
2021-05-15 08:16
cc47aff4
View on Github →
feat(algebra/homology): truncation and augmentation of chain complexes (
#7480
)
Estimated changes
Created
src/algebra/homology/augment.lean
added
def
chain_complex.augment
added
theorem
chain_complex.augment_X_succ
added
theorem
chain_complex.augment_X_zero
added
theorem
chain_complex.augment_d_one_zero
added
theorem
chain_complex.augment_d_succ_succ
added
def
chain_complex.augment_truncate
added
theorem
chain_complex.augment_truncate_hom_f_succ
added
theorem
chain_complex.augment_truncate_hom_f_zero
added
theorem
chain_complex.augment_truncate_inv_f_succ
added
theorem
chain_complex.augment_truncate_inv_f_zero
added
theorem
chain_complex.cochain_complex_d_succ_succ_zero
added
def
chain_complex.to_single₀_as_complex
added
def
chain_complex.truncate
added
def
chain_complex.truncate_augment
added
theorem
chain_complex.truncate_augment_hom_f
added
theorem
chain_complex.truncate_augment_inv_f
added
def
chain_complex.truncate_to