English
The linear combination over a restricted family s.restrict v equals the composition of linearCombinationOn with an equivalence between the restricted index set and its supported finsupp, followed by the subtype map.
Русский
Линейная комбинация по ограниченной семье s.restrict v равна композиции linearCombinationOn с эквивалентностью между ограниченным индексовым набором и поддерживаемым финспупом, далее идёт отображение подтипов.
LaTeX
$$$\\operatorname{linearCombination}_R(s.\\text{restrict } v) = \\operatorname{Submodule.subtype} _ \\circ\\! \\operatorname{linearCombinationOn}_R\\;(\\alpha)\\;M\\;R\\;v\\;s \\circ\\! (\\mathrm{supportedEquivFinsupp}\\; s)^{-\\!1}$$$
Lean4
theorem linearCombination_restrict (s : Set α) :
linearCombination R (s.restrict v) =
Submodule.subtype _ ∘ₗ linearCombinationOn α M R v s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap :=
by classical ext; simp [linearCombinationOn]
