toTensorAlgebra_tprod — Mathlib

English

The embedding sends the tprod of a Fin-n family to the corresponding tensor product in the algebra.

Русский

Встраивание переводит tprod семейства из Fin n в соответствующий тензорный продукт в алгебре.

LaTeX

$$$ TensorPower.toTensorAlgebra (PiTensorProduct.tprod R x) = TensorAlgebra.tprod R M n x $$$

Lean4

@[simp]
theorem toTensorAlgebra_tprod {n} (x : Fin n → M) :
    TensorPower.toTensorAlgebra (PiTensorProduct.tprod R x) = TensorAlgebra.tprod R M n x :=
  PiTensorProduct.lift.tprod _

Похожие утверждения