hilbertPoly_succ — Mathlib

English

The Hilbert polynomial of p for degree d+1 equals the sum over the support of p of coeff(i) times preHilbertPoly(F,d,i).

Русский

Хилбертов полином p в степени d+1 равен сумме по поддержке p от коэффициентов умноженных на preHilbertPoly(F,d,i).

LaTeX

$$$\operatorname{hilbertPoly}(p, d+1) = \sum_{i \in \operatorname{supp}(p)} p_i \cdot \operatorname{preHilbertPoly}(F, d, i)$$$

Lean4

theorem hilbertPoly_succ (p : F[X]) (d : ℕ) :
    hilbertPoly p (d + 1) = ∑ i ∈ p.support, (p.coeff i) • preHilbertPoly F d i :=
  rfl

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