English
The matrix representing the identity linear map on M1 with respect to basis v1 and v2 is the identity matrix when v1 = v2; more generally, the matrix of id is the identity under any basis pairing when considered appropriately.
Русский
Матрица, представляющая тождественное отображение на M1 относительно базиса v1 и v2, равна единичной матрице при совпадении базисов; в общем случае представление тождества сохраняется в матричном виде.
LaTeX
$$$\\text{toMatrix } v_1 v_1 \\; \\text{id} = 1.$$$
Lean4
/-- This will be a special case of `LinearMap.toMatrix_id_eq_basis_toMatrix`. -/
theorem toMatrix_id : LinearMap.toMatrix v₁ v₁ id = 1 :=
by
ext i j
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]
