kronecker_smul — Mathlib

English

Right scalar action distributes over Kronecker: A ⊗ (r • B) = r • (A ⊗ B).

Русский

Правое скалярное действие распределяется над кронекеровым произведением: A ⊗ (r • B) = r • (A ⊗ B).

LaTeX

$$A ⊗ (r \\cdot B) = r \\cdot (A ⊗ B)$$

Lean4

theorem kronecker_smul [Mul α] [SMul R α] [SMulCommClass R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
    A ⊗ₖ (r • B) = r • A ⊗ₖ B :=
  kroneckerMap_smul_right _ _ (fun _ _ => mul_smul_comm _ _ _) _ _

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