kroneckerTMulAlgEquiv_symm_single_tmul

English

The basic tensor of two single-entry matrices maps to the corresponding Kronecker product of those entries.

Русский

Базовый тензор двух одномерных матриц отображается в соответствующий Кронекеров произведение этих элементов.

LaTeX

$$$ kroneckerTMulLinearEquiv(a \otimes b) = a \otimes_\mathrm{K} b $$$

Lean4

@[simp]
theorem kroneckerTMulAlgEquiv_symm_single_tmul (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) :
    (kroneckerTMulLinearEquiv l m n p R S M N).symm (single (ia, ib) (ja, jb) (a ⊗ₜ b)) =
      single ia ja a ⊗ₜ single ib jb b :=
  by rw [LinearEquiv.symm_apply_eq, kroneckerTMulLinearEquiv_tmul, single_kroneckerTMul_single]

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