kronecker_mulVec_vec

Mathlib.LinearAlgebra.Matrix.Vec

URI: https://scilib.ai/kg/mathlib#Matrix.kronecker_mulVec_vec

← MathLib Explorer

English

For general A, X, B, vec Xᵥ*(B ⊗ₖ A) equals vec(A^T X B).

Русский

Для любых A, 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 kronecker_mulVec_vec (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R) :
    (B ⊗ₖ A) *ᵥ vec X = vec (A * X * Bᵀ) :=
  kronecker_mulVec_vec_of_commute _ _ _ fun _ _ _ => Commute.all _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru