mem_span_support — Mathlib

English

For an additive zero-based group G, any f in k[G] lies in the span of the images of its support under the natural inclusion.

Русский

Для аддитивной группы G (с нулем) любое f в k[G] лежит в спане образов его опоры при естественном включении.

LaTeX

$$$f \\in \\operatorname{span}_k (\\{ \\operatorname{of}(g) : g \\in \\operatorname{supp}(f) \\})$$$

Lean4

/-- An element of `k[G]` is in the submodule generated by its support. -/
theorem mem_span_support [AddZeroClass G] (f : k[G]) : f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
  erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

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