English
An element x lies in span_K s iff there exists a finitely supported c: M → K with c.support ⊆ s, c.sum α = x, and c.support.card ≤ finrank K (span K s).
Русский
Элемент x принадлежит span_K s тогда и только тогда, когда существует конечно поддерживаемая функция c: M → K такая, что c.support ⊆ s, сумма c равна x и карточность поддержки ≤ finrank K(span_K s).
LaTeX
$$$x \\in \\operatorname{span} K s \\iff \\exists c : M \\to_0 K, c.{\\text{support}}.card \\le \\operatorname{finrank} K (\\operatorname{span} K s) \\land c.{\\text{support}} \\subseteq s \\land c.sum (\\lambda m r, r \\cdot m) = x$$$
Lean4
instance instDFinsupp : Module.Finite R (Π₀ (i : ι), M i) :=
letI : Fintype ι := Fintype.ofFinite _
Module.Finite.equiv DFinsupp.linearEquivFunOnFintype.symm
