hilbertPoly_zero_left — Mathlib

English

For every natural d, the Hilbert polynomial of the zero polynomial is zero.

Русский

Для каждого натурального d хилбертов полином нулевого многочлена равен нулю.

LaTeX

$$$\forall d \in \mathbb{N},\; \operatorname{hilbertPoly}(0, d) = 0$$$

Lean4

theorem hilbertPoly_zero_left (d : ℕ) : hilbertPoly (0 : F[X]) d = 0 := by delta hilbertPoly;
  induction d with
  | zero => simp only
  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]

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