Commit 2021-01-07 13:09 87ef7aff

feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules (#5311) This PR defines the tensor product of an indexed family s : ι → Type* of semimodules over commutative semirings. We denote this space by ⨂[R] i, s i and define it as free_add_monoid (R × Π i, s i) quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in linear_algebra/tensor_product.lean.