mk — Mathlib · SciLib

English

Every element of the direct sum is the finite sum of its nonzero components along the universal finite index set.

Русский

Любой элемент прямой суммы является конечной суммой своих ненулевых компонент по универсальному конечному индексу.

LaTeX

$$$x = \\sum_{i\\in F} \\; \\mathrm{of}\\,β_i\\,(x_i)$ for a finite set F.$$

Lean4

/-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
and has coefficient `x i` for `i` in `s`. -/
def mk (s : Finset ι) : (∀ i : (↑s : Set ι), β i.1) →+ ⨁ i, β i
    where
  toFun := DFinsupp.mk s
  map_add' _ _ := DFinsupp.mk_add
  map_zero' := DFinsupp.mk_zero

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