mathlib

87ef7aff - feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules (#5311)

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`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>