toLinAlgEquiv_symm — Mathlib

English

The inverse of the algebra equivalence matrix-to-linear-map sends a linear map back to its matrix: (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

@[simp]
theorem toLinAlgEquiv_symm : (Matrix.toLinAlgEquiv v₁).symm = LinearMap.toMatrixAlgEquiv v₁ :=
  rfl

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