mul_kronecker_mul — Mathlib

English

The Kronecker product respects matrix multiplication: (A B) ⊗ (A' B') = (A ⊗ A') (B ⊗ B').

Русский

Кронекерово произведение сохраняет умножение матриц: (AB) ⊗ (A'B') = (A ⊗ A') (B ⊗ B').

LaTeX

$$$$ (A B) \\otimes_K (A' B') = (A \\otimes_K A') (B \\otimes_K B') $$$$

Lean4

theorem mul_kronecker_mul [Fintype m] [Fintype m'] [CommSemiring α] (A : Matrix l m α) (B : Matrix m n α)
    (A' : Matrix l' m' α) (B' : Matrix m' n' α) : (A * B) ⊗ₖ (A' * B') = A ⊗ₖ A' * B ⊗ₖ B' :=
  kroneckerMapBilinear_mul_mul (Algebra.lmul ℕ α).toLinearMap mul_mul_mul_comm A B A' B'

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