toLin_symm — Mathlib

English

The linear equivalence given by toLin has inverse given by toMatrix; applying toLin to a matrix and then taking its matrix back yields the original linear map, and vice versa.

Русский

Линейное эквивалентное отображение, задаваемое toLin, имеет обратное отображение через toMatrix; последовательное применение toLin к матрице и возврат через toMatrix восстанавливает исходное линейное отображение, и наоборот.

LaTeX

$$$\\text{toLin } v_1 v_2 \\; \\dashv\\vdash\\; \\text{toMatrix } v_1 v_2$ (взаимно обратны).$$

Lean4

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

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