kroneckerTMul_assoc' — Mathlib

English

A refined form of associativity expressed via a simplified equality after applying a submatrix equivalence.

Русский

Упрощённая форма ассоциативности, выраженная через подматрицу и эквивалентности индексов.

LaTeX

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

Lean4

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

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