kronecker_add — Mathlib

English

The 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) ⊗ B = A1 ⊗ B + A2 ⊗ B$$

Lean4

theorem kronecker_add [Distrib α] (A : Matrix l m α) (B₁ B₂ : Matrix n p α) : A ⊗ₖ (B₁ + B₂) = A ⊗ₖ B₁ + A ⊗ₖ B₂ :=
  kroneckerMap_add_right _ mul_add _ _ _

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