kronecker_mulVec_vec_of_commute — Mathlib

English

The vectorization of a product equals a Kronecker product action on vec: vec(A B) = (1 ⊗ A) vec(B).

Русский

Векторизация произведения матриц равна действию (1 ⊗ A) на vec(B).

LaTeX

$$$$\operatorname{vec}(A B) = (1 \otimes A) \operatorname{vec}(B)$$$$

Lean4

/-- Technical lemma shared with `kronecker_mulVec_vec` and `vec_mul_eq_mulVec`. -/
theorem kronecker_mulVec_vec_of_commute (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R)
    (hB : ∀ x i j, Commute x (B i j)) : (B ⊗ₖ A) *ᵥ vec X = vec (A * X * Bᵀ) :=
  by
  ext ⟨k, l⟩
  simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply, ←
    Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]

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