single_kroneckerTMul_single — Mathlib

English

Kronecker product of a single-entry matrix is the corresponding single-entry matrix in the product space: single i1 j1 a ⊗ single i2 j2 b = single (i1,i2) (j1,j2) (a ⊗ b).

Русский

Кронекерово произведение одиночной матрицы равно одиночной матрице в произведённом пространстве: single i1 j1 a ⊗ single i2 j2 b = single (i1,i2) (j1,j2) (a ⊗ b).

LaTeX

$$single i1 j1 a ⊗ₖₜ[R] single i2 j2 b = single (i1, i2) (j1, j2) (a ⊗ₜ b)$$

Lean4

theorem single_kroneckerTMul_single [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (i₁ : l) (j₁ : m)
    (i₂ : n) (j₂ : p) (a : α) (b : β) : single i₁ j₁ a ⊗ₖₜ[R] single i₂ j₂ b = single (i₁, i₂) (j₁, j₂) (a ⊗ₜ b) :=
  kroneckerMap_single_single _ _ _ _ _ (zero_tmul _) (tmul_zero _) _ _

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