TensorPower.list_prod_gradedMonoid_mk_single

theorem TensorPower.list_prod_gradedMonoid_mk_single : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ) (x : Fin n → M), (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod = GradedMonoid.mk n ((PiTensorProduct.tprod R) x)

This theorem states that, given a commutative semiring `R` and an additive commutative monoid `M` that is also an `R`-module, and given a map `x` from a finite set of size `n` to `M`, the product of tensor products where each tensor product is made from a single vector (specifically, each vector `x a` where `a` ranges over the finite set, and we mean the tensor product in the sense of `PiTensorProduct.tprod R`) is the same as a single tensor product of all the vectors `x a`. This tensor product is encoded as a `GradedMonoid.mk` where the grade is the size of the finite set (for the product of single-vector tensor products) or `n` (for the single tensor product of all vectors).

More concisely: Given a commutative semiring `R`, an additive commutative `R`-module `M`, and a finite map `x` from a set of size `n` to `M`, the product of tensor products of `x a` for all `a` in the set is equal to the single tensor product of all `x a` in `M⊗⁗⁡_R (n: ℕ)`.