ofFinsupp_sum — Mathlib

English

The embedding preserves finite sums: ⟨∑ i∈s f i⟩ = ∑ i∈s ⟨f i⟩.

Русский

Встраивание сохраняет конечные смеси: ⟨∑ i∈s f_i⟩ = ∑ i∈s ⟨f_i⟩.

LaTeX

$$$\Bigl\langle \sum_{i\in s} f_i \Bigr\rangle = \sum_{i\in s} \langle f_i \rangle$$$

Lean4

theorem ofFinsupp_sum {ι : Type*} (s : Finset ι) (f : ι → R[ℕ]) : (⟨∑ i ∈ s, f i⟩ : R[X]) = ∑ i ∈ s, ⟨f i⟩ :=
  map_sum (toFinsuppIso R).symm f s

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