toLinAlgEquiv_toMatrixAlgEquiv — Mathlib

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]

Похожие утверждения