range_toLin' — Mathlib

English

The range (image) of the linear map corresponding to M equals the span of the column vectors of M.

Русский

Образ линейного отображения, соответствующего матрице M, равен линейной оболочке столбцов M.

LaTeX

$$$ \\mathrm{range}(\\mathrm{toLin'}(M)) = \\mathrm{span}_R\\bigl(\\mathrm{range}(M_{\\cdot})\\bigr) $$$

Lean4

theorem range_toLin' (M : Matrix m n R) : LinearMap.range (Matrix.toLin' M) = span R (range M.col) :=
  Matrix.range_mulVecLin _

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