mathlib3

061d04b9 - feat(category_theory/monoidal): distribute tensor over direct sum (#12626)

feat(category_theory/monoidal): distribute tensor over direct sum (#12626) This is preliminary to the monoidal structure on chain complexes. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>