vec_vecMul_kronecker — Mathlib

English

For A, X, B with commuting entries, vec Xᵥ* (B ⊗ₖ A) = vec(A^T X B).

Русский

При заданных условиях коммьютирования элементов, vec Xᵥ* (B ⊗ₖ A) = vec(A^T X B).

LaTeX

$$$$\operatorname{vec} X \_v* (B \otimes_{k} A) = \operatorname{vec}(A^{\top} X B)$$$$

Lean4

theorem vec_vecMul_kronecker (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R) :
    vec X ᵥ* (B ⊗ₖ A) = vec (Aᵀ * X * B) :=
  vec_vecMul_kronecker_of_commute _ _ _ fun _ _ _ => Commute.all _ _

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