add_kroneckerTMul — Mathlib

English

Kronecker product distributes over addition in the left factor: (A1 + A2) ⊗ B = A1 ⊗ B + A2 ⊗ B.

Русский

Кронекерово произведение распределяется по сложению слева: (A1 + A2) ⊗ B = A1 ⊗ B + A2 ⊗ B.

LaTeX

$$(A1 + A2) ⊗_R B = A1 ⊗_R B + A2 ⊗_R B$$

Lean4

theorem add_kroneckerTMul (A₁ A₂ : Matrix l m α) (B : Matrix n p α) : (A₁ + A₂) ⊗ₖₜ[R] B = A₁ ⊗ₖₜ B + A₂ ⊗ₖₜ B :=
  kroneckerMap_add_left _ add_tmul _ _ _

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