English
For any f in the monoid algebra k[G], f lies in the submodule generated by the elements obtained from its support via the canonical injection. Equivalently, f is a linear combination of the basis elements indexed by its support.
Русский
Для любого f в моноидной алгебре k[G] выполняется, что f лежит в подмодуле, порождаемом образами опоры f через каноническое вложение. Эквивалентно, f является линейной комбинацией базисных элементов, индексированных по опоре f.
LaTeX
$$$f \\in \\operatorname{span}_k\\{ \\operatorname{of}(g) \\mid g \\in \\operatorname{supp}(f) \\}$$$
Lean4
/-- An element of `MonoidAlgebra k G` is in the subalgebra generated by its support. -/
theorem mem_span_support (f : MonoidAlgebra k G) : f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]
