toDirectSum_single — Mathlib

English

Using the unbundled inclusion, f ∈ k[G] lies in the span of the images of its support.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toDirectSum_single (i : ι) (m : M) : AddMonoidAlgebra.toDirectSum (Finsupp.single i m) = DirectSum.of _ i m :=
  Finsupp.toDFinsupp_single i m

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