vec_mul_eq_mulVec — Mathlib

English

For 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 vec_mul_eq_mulVec [DecidableEq n] (A : Matrix l m R) (B : Matrix m n R) : vec (A * B) = (1 ⊗ₖ A) *ᵥ vec B :=
  by
  rw [kronecker_mulVec_vec_of_commute, transpose_one, Matrix.mul_one]
  intro x i j
  obtain rfl | hij := eq_or_ne i j <;> simp [*]

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