kroneckerTMul_add — Mathlib

English

Kronecker product distributes over addition in the right factor: A ⊗ (B1 + B2) = A ⊗ B1 + A ⊗ B2.

Русский

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

LaTeX

$$A ⊗_R (B1 + B2) = A ⊗_R B1 + A ⊗_R B2$$

Lean4

theorem kroneckerTMul_add (A : Matrix l m α) (B₁ B₂ : Matrix n p β) : A ⊗ₖₜ[R] (B₁ + B₂) = A ⊗ₖₜ B₁ + A ⊗ₖₜ B₂ :=
  kroneckerMap_add_right _ tmul_add _ _ _

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