tensorProduct_repr_tmul_apply — Mathlib

English

The repr of a pure tensor m ⊗ n with respect to the tensor product basis is given by the product of the component representations.

Русский

Обратное отображение по базису тензорного произведения применяется к простому тензору и даёт произведение представлений составляющих.

LaTeX

$$$ (\text{tensorProduct}(b,c).repr (m \otimes n)) (i,j) = c.repr(n)(j) \cdot b.repr(m)(i) $$$

Lean4

@[simp]
theorem tensorProduct_repr_tmul_apply (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
    (tensorProduct b c).repr (m ⊗ₜ n) (i, j) = c.repr n j • b.repr m i := by simp [tensorProduct]

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