toDirectSum — Mathlib

English

Every element of k[G] is contained in the span of the basis elements corresponding to its support.

Русский

Каждый элемент k[G] лежит в спане базисных элементов, индексированных по своей опоре.

LaTeX

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

Lean4

/-- Interpret an `AddMonoidAlgebra` as a homogeneous `DirectSum`. -/
def toDirectSum [Semiring M] (f : AddMonoidAlgebra M ι) : ⨁ _ : ι, M :=
  Finsupp.toDFinsupp f

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