mathlib3

775edc61 - feat(linear_algebra/tensor_product): Inherit smul through is_scalar_tower (#5317)

feat(linear_algebra/tensor_product): Inherit smul through is_scalar_tower (#5317) Most notably, this now means that the lemmas about `smul` and `tmul` can be used to prove `∀ z : Z, (z • a) ⊗ₜ[R] b = z • (a ⊗ₜ[R] b)`. Hopefully these instances aren't dangerous - in particular, there's now a risk of a non-defeq-but-eq diamond for the `ℤ`- and `ℕ`-module structure. However: * this diamond already exists in other places anyway * the diamond if it comes up can be solved with `subsingleton.elim`, since we have a proof that all Z-module and N-module structures must be equivalent.