eval₂_sum — Mathlib

English

Evaluation is linear over finite sums: eval₂ f g (∑ x∈s, p x) = ∑ x∈s, eval₂ f g (p x).

Русский

Оценка линейна по суммам: eval₂ f g (∑ x∈s p x) = ∑ x∈s eval₂ f g (p x).

LaTeX

$$$\\mathrm{eval}_2 f g\\left(\\sum_{x\\in s} p(x)\\right) = \\sum_{x\\in s} \\mathrm{eval}_2 f g\\left(p(x)\\right)$$$

Lean4

@[simp]
theorem eval₂_sum (s : Finset S₂) (p : S₂ → MvPolynomial σ R) : eval₂ f g (∑ x ∈ s, p x) = ∑ x ∈ s, eval₂ f g (p x) :=
  map_sum (eval₂Hom f g) _ s

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