kronecker_assoc — Mathlib

English

The Kronecker product is associative on the nose up to an index reordering: reindex(prodAssoc l n q)(prodAssoc m p r)(A ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C).

Русский

Кронекерово произведение ассоциативно с точностью до перестановки индексов.

LaTeX

$$$\text{kroneckerAssoc} (A,B,C) : \text{reindex} (\mathrm{Equiv.prodAssoc}\ l\ n\ q) (\mathrm{Equiv.prodAssoc}\ m\ p\ r) (A ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C)$$$

Lean4

theorem kronecker_assoc [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
    reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (A ⊗ₖ B ⊗ₖ C) = A ⊗ₖ (B ⊗ₖ C) :=
  kroneckerMap_assoc₁ _ _ _ _ A B C mul_assoc

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