toLin'_toMatrix' — Mathlib

English

The forward and inverse directions between matrices and linear maps establish a linear equivalence.

Русский

Прямое и обратное направления между матрицами и линейными отображениями образуют линейное эквивалентное отображение.

LaTeX

$$theorem toLin'_toMatrix' (f : (n → R) →ₗ[R] m → R) : Matrix.toLin' (LinearMap.toMatrix' f) = f$$

Lean4

@[simp]
theorem toLin'_toMatrix' (f : (n → R) →ₗ[R] m → R) : Matrix.toLin' (LinearMap.toMatrix' f) = f :=
  Matrix.toLin'.apply_symm_apply f

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