Commit 2020-12-18 15:15 775edc61

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.