mul_kroneckerTMul_mul — Mathlib

English

Kronecker product commutes with matrix multiplication componentwise: (A B) ⊗ (A' B') = A ⊗ A' · B ⊗ B'.

Русский

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

LaTeX

$$ (A * B) ⊗ₖₜ[R] (A' * B') = A ⊗ₖₜ[R] A' * B ⊗ₖₜ[R] B'$$

Lean4

theorem mul_kroneckerTMul_mul [NonUnitalSemiring α] [NonUnitalSemiring β] [Module R α] [Module R β]
    [IsScalarTower R α α] [SMulCommClass R α α] [IsScalarTower R β β] [SMulCommClass R β β] [Fintype m] [Fintype m']
    (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) :
    (A * B) ⊗ₖₜ[R] (A' * B') = A ⊗ₖₜ[R] A' * B ⊗ₖₜ[R] B' :=
  kroneckerMapBilinear_mul_mul (TensorProduct.mk R α β) tmul_mul_tmul A B A' B'

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