English
For a matrix M, the range of vecMulLinear equals the span of the rows of M.
Русский
Область значений vecMulLinear матрицы M равна линейной оболочке строк M.
LaTeX
$$LinearMap.range M.vecMulLinear = span R (range M.row)$$
Lean4
theorem range_vecMulLinear (M : Matrix m n R) : LinearMap.range M.vecMulLinear = span R (range M.row) :=
by
letI := Classical.decEq m
simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ← Ideal.span_singleton_one, Ideal.span,
Submodule.map_span, image_image, image_singleton, Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion,
iUnion_singleton_eq_range, LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]
unfold vecMul
simp_rw [single_dotProduct, one_mul]
