kronecker_assoc' — Mathlib

English

A version of associativity with a submatrix equality adjusted by swap of prodAssoc indices.

Русский

Версия ассоциативности с подматрицей, скорректированная перестановкой индексов.

LaTeX

$$$\text{kronecker_assoc'} (A,B,C) : \submatrix (A ⊗ₖ B ⊗ₖ C) (\mathrm{prodAssoc}\ l\ n\ q)^{-1} (\mathrm{prodAssoc}\ m\ p\ r)^{-1} = A ⊗ₖ B ⊗ₖ C$$$

Lean4

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

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