toMatrixAlgEquiv_transpose_apply'

English

The inverse of the matrix-to-linear-map equivalence corresponds to the matrix-to-linear-map equivalence in the opposite direction: (Matrix.toLinAlgEquiv v1)^{-1} = LinearMap.toMatrixAlgEquiv v1.

Русский

Обратная к матрично-линейному соответствию эквивалентность соответствует эквивалентности в противоположном направлении: (Matrix.toLinAlgEquiv v1)^{-1} = LinearMap.toMatrixAlgEquiv v1.

LaTeX

$$$(\mathrm{toLinAlgEquiv}_{v_1})^{-1} = \mathrm{toMatrixAlgEquiv}_{v_1}$$$

Lean4

theorem toMatrixAlgEquiv_transpose_apply' (f : M₁ →ₗ[R] M₁) (j : n) :
    (LinearMap.toMatrixAlgEquiv v₁ f)ᵀ j = v₁.repr (f (v₁ j)) :=
  LinearMap.toMatrixAlgEquiv_transpose_apply v₁ f j

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