Commit 2021-01-06 16:21 91fcb480

feat(linear_algebra/tensor_product,algebra/module/linear_map): Made tmul_smul and map_smul_of_tower work for int over semirings (#5430) With this change, ∀ (f : M →ₗ[S] M₂) (z : int) (x : M), f (z • x) = z • f x can be proved with linear_map.map_smul_of_tower even when S is a semiring, and z • (m ⊗ₜ n : M ⊗[S] N) = (r • m) ⊗ₜ n can be proved with tmul_smul.