ofReal_finsupp_sum — Mathlib

English

For a finsupp f from α to M and g: α → M → ℝ, the embedding commutes with finsupp sums: ((f.sum (λ a b, g a b) : ℝ) : K) = f.sum (λ a b, RCLike.ofReal (g a b)).

Русский

Для функционала finsupp f : α →₀ M и функции g : α → M → ℝ отображение сохраняет сумму: ((f.sum (λ a b, g a b) : ℝ) : K) = ∑_{a,b} RCLike.ofReal (g a b).

LaTeX

$$$((f.sum\, fun\ a\ b\, => g\ a\ b : \mathbb{R}) : K) = f.sum\, fun\ a\ b\, => RCLike.ofReal (g\ a\ b)$$$

Lean4

@[simp, rclike_simps, norm_cast]
theorem ofReal_finsupp_sum {α M : Type*} [Zero M] (f : α →₀ M) (g : α → M → ℝ) :
    ((f.sum fun a b => g a b : ℝ) : K) = f.sum fun a b => (g a b : K) :=
  map_finsuppSum (algebraMap ℝ K) f g

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