kroneckerTMul_assoc — Mathlib

English

Kronecker product is associative up to a canonical reindexing using the TensorProduct associativity isomorphism.

Русский

Кронекерово произведение ассоциативно до естественного перераспределения индексов через изоморфизм ассоциации тензорного произведения.

LaTeX

$$reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r) (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ)) = A ⊗ₖₜ[R] B ⊗ₖₜ[R] C$$

Lean4

theorem kroneckerTMul_assoc (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
    reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)
        (((A ⊗ₖₜ[R] B) ⊗ₖₜ[R] C).map (TensorProduct.assoc R α β γ)) =
      A ⊗ₖₜ[R] B ⊗ₖₜ[R] C :=
  ext fun _ _ => assoc_tmul _ _ _

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