ofDirectSum_of_tprod — Mathlib

English

For a vector x in the nth tensor power, applying the canonical direct-sum map to the tprod of x equals the tprod in the tensor algebra.

Русский

Для вектора x в n-й тензорной степени применение канонического отображения прямой суммы к tprod(x) даёт tprod в тензорной алгебре.

LaTeX

$$$ ofDirectSum (DirectSum.of _ n (PiTensorProduct.tprod R x)) = tprod R M n x $$$

Lean4

@[simp]
theorem ofDirectSum_of_tprod {n} (x : Fin n → M) :
    ofDirectSum (DirectSum.of _ n (PiTensorProduct.tprod R x)) = tprod R M n x :=
  (DirectSum.toAddMonoid_of (fun _ ↦ LinearMap.toAddMonoidHom TensorPower.toTensorAlgebra) _ _).trans
    (TensorPower.toTensorAlgebra_tprod _)

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