range_mulVecLin — Mathlib

English

The range of mulVecLin equals the span of the range of the matrix columns.

Русский

Образ отображения mulVecLin равен линейной оболочке множества значений столбцов матрицы.

LaTeX

$$Matrix.range M.mulVecLin = span R (range M.col)$$

Lean4

theorem range_mulVecLin (M : Matrix m n R) : LinearMap.range M.mulVecLin = span R (range M.col) := by
  rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]

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