English
If every entry of A commutes with every entry of B, then vec(X) acted by B ⊗ A equals vec(A^T X B).
Русский
Если каждый элемент A коммутирует с каждым элементом B, тогда vec(X) под действием B ⊗ A даёт vec(A^T X B).
LaTeX
$$$$\operatorname{vec}(X)^{\top} (B \otimes_{k} A) = \operatorname{vec}(A^{\top} X B)$$$$
Lean4
/-- Technical lemma shared with `vec_vecMul_kronecker` and `vec_mul_eq_vecMul`. -/
theorem vec_vecMul_kronecker_of_commute (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R)
(hA : ∀ x i j, Commute (A i j) x) : vec X ᵥ* (B ⊗ₖ A) = vec (Aᵀ * X * B) :=
by
ext ⟨k, l⟩
simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply, ←
Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
