English
The matrix corresponding to TensorProduct.assoc is a permutation of the identity given by the prodAssoc equivalence.
Русский
Матрица, соответствующая TensorProduct.assoc, является перестановкой единицы согласно эквивалентности prodAssoc.
LaTeX
$$toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP)) (TensorProduct.assoc R M N P) = (1 : Matrix (ι × κ × τ) (ι × κ × τ) R).submatrix _root_.id (Equiv.prodAssoc ι κ τ)$$
Lean4
/-- `TensorProduct.assoc` corresponds to a permutation of the identity matrix. -/
theorem toMatrix_assoc :
toMatrix ((bM.tensorProduct bN).tensorProduct bP) (bM.tensorProduct (bN.tensorProduct bP))
(TensorProduct.assoc R M N P) =
(1 : Matrix (ι × κ × τ) (ι × κ × τ) R).submatrix _root_.id (Equiv.prodAssoc _ _ _) :=
by
ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, assoc_tmul,
Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ k', @eq_comm _ j',
smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, @eq_comm _ i', submatrix_apply, Matrix.one_apply, id_eq,
Equiv.prodAssoc_apply, Prod.mk.injEq]
