Theorems · Definition · commutative algebra

Polynomial.preHilbertPoly

(F : Type u_1) → [inst : Field F] → ℕ → ℕ → Polynomial F

For any field F and natural numbers d and k, Polynomial.preHilbertPoly F d k is defined as (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1)). This is the most basic form of Hilbert polynomials. Polynomial.preHilbertPoly ℚ d 0 is exactly the Hilbert polynomial of the polynomial ring ℚ[X_0,...,X_d] viewed as a graded module over itself. In fact, Polynomial.preHilbertPoly F d k is the same as Polynomial.hilbertPoly ((X : F[X]) ^ k) (d + 1) for any field F and d k : ℕ (see the lemma Polynomial.hilbertPoly_X_pow_succ). See also the lemma Polynomial.preHilbertPoly_eq_choose_sub_add, which states that if CharZero F, then for any d k n : ℕ with k ≤ n, (Polynomial.preHilbertPoly F d k).eval (n : F) equals (n - k + d).choose d.

Defined in

Mathlib.RingTheory.Polynomial.HilbertPoly

Cited by

11 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Field