mathlib
7f46c811 - feat(chain_complex): lemmas about eq_to_hom (#6250)

Commit
4 years ago
feat(chain_complex): lemmas about eq_to_hom (#6250) Adds two lemmas relating `eq_to_hom` to differentials and chain maps. Useful in the ubiquitous circumstance of having to apply identities in the index of a chain complex. Also add some `@[reassoc]` tags for convenience. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading