eval₂_eq' — Mathlib

English

If the index set is finite, eval₂ can be written with a universal product over all indices.

Русский

При конечном индексовом множестве eval₂ может быть записан через произведение по всем индексам.

LaTeX

$$$f.eval_2\, g\, X\, p = \sum_{d \in \mathrm{support}(p)} g(p_d) \cdot \prod_{i} X_i^{d(i)}$$$

Lean4

theorem eval₂_eq' [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
    f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i, X i ^ d i :=
  by
  simp only [eval₂_eq, ← Finsupp.prod_pow]
  rfl

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