mathlib

930485c1 - feat(linear_algebra/tensor_product): distrib_mul_actions are inherited (#7516)

feat(linear_algebra/tensor_product): distrib_mul_actions are inherited (#7516) It turns out that `tensor_product.has_scalar` requires only `distrib_mul_action` and not `semimodule` on its components. As a result, a tensor product can inherit the `distrib_mul_action` structure of its components too. Notably, this would enable `has_scalar (units R) (M ⊗[R] N)` in future.