Commit 2021-02-23 14:09 7f46c811

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.