Products of pure tensors

In the tensor product A ⊗[R] B of commutative R-algebras, a finite product of pure tensors is the pure tensor of the products: ∏ i ∈ s, a i ⊗ₜ b i = (∏ i ∈ s, a i) ⊗ₜ ∏ i ∈ s, b i. This is the multiplicative counterpart of TensorProduct.sum_tmul and TensorProduct.tmul_sum, and extends Algebra.TensorProduct.tmul_pow from powers to products. For ordered list products neither factor needs to be commutative.

theorem List.prod_map_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (l : List ι) (a : ι → A) (b : ι → B) : (map (fun (i : ι) => a i ⊗ₜ[R] b i) l).prod = (map a l).prod ⊗ₜ[R] (map b l).prod

The ordered product of pure tensors is the pure tensor of the ordered products. Neither algebra is required to be commutative.

@[simp]

theorem Algebra.TensorProduct.prod_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] (s : Finset ι) (a : ι → A) (b : ι → B) : ∏ i ∈ s, a i ⊗ₜ[R] b i = (∏ i ∈ s, a i) ⊗ₜ[R] ∏ i ∈ s, b i

A finite product of pure tensors is the pure tensor of the products.

theorem Algebra.TensorProduct.list_prod_ofFn_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [Semiring B] [Algebra R B] {n : ℕ} (a : Fin n → A) (b : Fin n → B) : (List.ofFn fun (t : Fin n) => a t ⊗ₜ[R] b t).prod = (∏ t : Fin n, a t) ⊗ₜ[R] (List.ofFn b).prod

The product of a list of pure tensors in A ⊗[R] B, with A commutative, is the pure tensor of the product of the left factors and the ordered product of the right factors.