mem_span_support — Mathlib

English

An element f lies in the k-span generated by the images of the support of f under the natural embedding of k G.

Русский

Элемент f лежит в k- Span, порождаемом образами опоры f через естественное вложение k G.

LaTeX

$$f \\in \\operatorname{Span}_k ( of\\ k\\ G '' (f.\\operatorname{support} : \\ Set\\ G))$$

Lean4

/-- An element of `SkewMonoidAlgebra k G` is in the subalgebra generated by its support. -/
theorem mem_span_support (f : SkewMonoidAlgebra k G) : f ∈ Submodule.span k (of k G '' (f.support : Set G)) :=
  by
  rw [Fintype.mem_span_image_iff_exists_fun k]
  use Finset.restrict f.support f.coeff
  simp [smul_single, ← sum_def', sum_single]

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