toLin' — Mathlib

English

The image of a matrix under the toLin' equivalence corresponds to the mulVecLin map.

Русский

Изображение матрицы через toLin' соответствует mulVecLin.

LaTeX

$$theorem toLin'_apply' (M : Matrix m n R) : Matrix.toLin' M = M.mulVecLin$$

Lean4

/-- A `Matrix m n R` is linearly equivalent to a linear map `(n → R) →ₗ[R] (m → R)`.

Note that the forward-direction does not require `DecidableEq` and is `Matrix.mulVecLin`. -/
def toLin' : Matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R :=
  LinearMap.toMatrix'.symm

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