English
The transpose of the matrix-to-linear-equivalence maps satisfies (toMatrixAlgEquiv v1 f).transpose j equals the j-th coordinate of the representation of f(v1 j); equivalently, (toLinAlgEquiv v1 f) i j matches the same coordinates.
Русский
Транспонированная матрица эквивалентности отображений соответствует j-ой координате представления вектора f(v1 j); иначе говоря, (toMatrixAlgEquiv v1 f).transpose j даёт ту же координату, что и (toLinAlgEquiv v1 f) i j.
LaTeX
$$$(\mathrm{toMatrixAlgEquiv}_{v_1} f)^{\mathrm{T}}_j = v_1.repr(f(v_1 j))_j$$$
Lean4
@[simp]
theorem toLinAlgEquiv_toMatrixAlgEquiv (f : M₁ →ₗ[R] M₁) :
Matrix.toLinAlgEquiv v₁ (LinearMap.toMatrixAlgEquiv v₁ f) = f := by
rw [← Matrix.toLinAlgEquiv_symm, AlgEquiv.apply_symm_apply]