Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 10:32 061d04b9

View on Github →

feat(category_theory/monoidal): distribute tensor over direct sum (#12626) This is preliminary to the monoidal structure on chain complexes.

Estimated changes

Modified src/category_theory/limits/shapes/biproducts.lean

added theorem category_theory.limits.is_bilimit.binary_total

added theorem category_theory.limits.is_bilimit.total

Modified src/category_theory/monoidal/category.lean

added theorem category_theory.monoidal_category.dite_tensor

added theorem category_theory.monoidal_category.tensor_dite

Modified src/category_theory/monoidal/preadditive.lean

added def category_theory.left_distributor

added theorem category_theory.left_distributor_assoc

added theorem category_theory.left_distributor_hom

added theorem category_theory.left_distributor_inv

added theorem category_theory.left_distributor_right_distributor_assoc

added def category_theory.right_distributor

added theorem category_theory.right_distributor_assoc

added theorem category_theory.right_distributor_hom

added theorem category_theory.right_distributor_inv

added theorem category_theory.sum_tensor

added theorem category_theory.tensor_sum