English
The matrix equivalence forms a genuine equivalence: left_inv and right_inv hold for the equivalence between Tensor product and matrices.
Русский
Эквивалентность между тензорным произведением и матрицами образует полноценное эквивалентное отображение: левый и правый инверсии выполняются.
LaTeX
$$$ toFunAlgHom \circ invFun = id_{Matrix\,n\,n\,A} \quad \text{and} \quad invFun \circ toFunAlgHom = id_{A \otimes M} $$$
Lean4
theorem right_inv (M : Matrix n n A) : (toFunAlgHom n R A) (invFun n R A M) = M :=
by
simp only [invFun, map_sum, toFunAlgHom_apply]
convert Finset.sum_product (β := Matrix n n A) ..
conv_lhs => rw [matrix_eq_sum_single M]
refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun j _ => Matrix.ext fun a b => ?_
dsimp [single]
split_ifs <;> aesop
