toMatrix_symm — Mathlib

English

The inverse of the matrix-to-linear-map equivalence is the linear-map-to-matrix equivalence; specifically (Matrix.toLin v1 v2).symm = LinearMap.toMatrix v1 v2 and conversely.

Русский

Обратной связью к соответствию матрица ↔ линейное отображение является обратное преобразование; то есть (Matrix.toLin v1 v2).symm = LinearMap.toMatrix v1 v2 и наоборот.

LaTeX

$$$\\big(\\text{Matrix.toLin } v_1 v_2\\big)^{-1} = \\text{LinearMap.toMatrix } v_1 v_2,$$ и симметрично.$$

Lean4

@[simp]
theorem toMatrix_symm : (LinearMap.toMatrix v₁ v₂).symm = Matrix.toLin v₁ v₂ :=
  rfl

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