range_linearCombination — Mathlib

English

The range of the finite-type linearCombination equals the span of the range of v: LinearMap.range (Fintype.linearCombination R v) = Span_R (range v).

Русский

Образ линейной комбинации для конечного числа индексов равен области порождаемых векторов: диапазон равен span самых значений v.

LaTeX

$$$\\operatorname{range} (\\mathrm{Fintype.linearCombination}_R v) = \\operatorname{span}_R(\\mathrm{Set.range}\,v)$$$

Lean4

@[simp]
theorem range_linearCombination : LinearMap.range (Fintype.linearCombination R v) = Submodule.span R (Set.range v) := by
  rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp, LinearEquiv.range,
    Submodule.map_top, Finsupp.range_linearCombination]

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