mem_span_support' — Mathlib

English

With unbundled inclusion, an element f in k[G] belongs to the span of the images of its support under the inclusion map.

Русский

С использованием раздельного включения элемент f ∈ k[G] принадлежит диапазону образов опоры f через отображение включения.

LaTeX

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

Lean4

/-- An element of `k[G]` is in the subalgebra generated by its support, using
unbundled inclusion. -/
theorem mem_span_support' (f : k[G]) : f ∈ Submodule.span k (of' k G '' (f.support : Set G)) :=
  by
  delta of'
  rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

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