English
Auxiliary matrix representations coincide with standard toMatrix₂ under the chosen bases; the auxiliary construction agrees with the canonical one.
Русский
Вспомогательные матричные представления совпадают с каноническими при выбранных базисах; конструкция согласуется.
LaTeX
$$$\mathrm{toMatrix}_{\!2\!Aux}(R)\ B = \mathrm{toMatrix}_2(R)\ B.$$$
Lean4
@[simp]
theorem toLinearMap₂_apply (M : Matrix n m N₂) (x : M₁) (y : M₂) :
Matrix.toLinearMap₂ b₁ b₂ M x y = ∑ i, ∑ j, b₁.repr x i • b₂.repr y j • M i j :=
Finset.sum_congr rfl fun _ _ =>
Finset.sum_congr rfl fun _ _ =>
smul_algebra_smul_comm ((RingHom.id R) ((Basis.equivFun b₁) x _)) ((RingHom.id R) ((Basis.equivFun b₂) y _))
(M _ _)
-- Not a `simp` lemma since `LinearMap.toMatrix₂` needs an extra argument
