toFinsupp_sum — Mathlib

English

The map toFinsuppIsoLinear gives an isomorphism of R-vector spaces between R[X] and R[ℕ], i.e., it is an R-linear equivalence.

Русский

Карта toFinsuppIsoLinear задаёт изоморфизм векторных пространств над R между R[X] и R[ℕ].

LaTeX

$$$\text{toFinsuppIsoLinear} : R[X] \cong_{\mathsf{R}} R[\mathbb{N}]$ is an $\mathbb{R}$-linear equivalence$$

Lean4

theorem toFinsupp_sum {ι : Type*} (s : Finset ι) (f : ι → R[X]) :
    (∑ i ∈ s, f i : R[X]).toFinsupp = ∑ i ∈ s, (f i).toFinsupp :=
  map_sum (toFinsuppIso R) f s

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