diff --git a/Mathlib.lean b/Mathlib.lean
index 380263015c62c..ac692cd27c721 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4481,6 +4481,7 @@ import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
 import Mathlib.RingTheory.Polynomial.GaussLemma
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
 import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
+import Mathlib.RingTheory.Polynomial.HilbertPoly
 import Mathlib.RingTheory.Polynomial.Ideal
 import Mathlib.RingTheory.Polynomial.IntegralNormalization
 import Mathlib.RingTheory.Polynomial.IrreducibleRing
diff --git a/Mathlib/Data/Nat/Factorial/BigOperators.lean b/Mathlib/Data/Nat/Factorial/BigOperators.lean
index 56a55af7e4af1..606f5b7c49b2d 100644
--- a/Mathlib/Data/Nat/Factorial/BigOperators.lean
+++ b/Mathlib/Data/Nat/Factorial/BigOperators.lean
@@ -33,6 +33,10 @@ theorem prod_factorial_dvd_factorial_sum : (∏ i ∈ s, (f i)!) ∣ (∑ i ∈
   · rw [prod_cons, Finset.sum_cons]
     exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)
 
+theorem ascFactorial_eq_prod_range (n : ℕ) : ∀ k, n.ascFactorial k = ∏ i ∈ range k, (n + i)
+  | 0 => rfl
+  | k + 1 => by rw [ascFactorial, prod_range_succ, mul_comm, ascFactorial_eq_prod_range n k]
+
 theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i ∈ range k, (n - i)
   | 0 => rfl
   | k + 1 => by rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]
diff --git a/Mathlib/RingTheory/Polynomial/HilbertPoly.lean b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean
new file mode 100644
index 0000000000000..302a9660f7465
--- /dev/null
+++ b/Mathlib/RingTheory/Polynomial/HilbertPoly.lean
@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2024 Fangming Li. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fangming Li, Jujian Zhang
+-/
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.RingTheory.Polynomial.Pochhammer
+import Mathlib.RingTheory.PowerSeries.WellKnown
+import Mathlib.Tactic.FieldSimp
+
+/-!
+# Hilbert polynomials
+
+In this file, we formalise the following statement: if `F` is a field with characteristic `0`, then
+given any `p : F[X]` and `d : ℕ`, there exists some `h : F[X]` such that for any large enough
+`n : ℕ`, `h(n)` is equal to the coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+This `h` is unique and is denoted as `Polynomial.hilbertPoly p d`.
+
+For example, given `d : ℕ`, the power series expansion of `1/(1-X)ᵈ⁺¹` in `F[X]` is
+`Σₙ ((d + n).choose d)Xⁿ`, which equals `Σₙ ((n + 1)···(n + d)/d!)Xⁿ` and hence
+`Polynomial.hilbertPoly (1 : F[X]) d` is the polynomial `(n + 1)···(n + d)/d!`. Note that
+if `d! = 0` in `F`, then the polynomial `(n + 1)···(n + d)/d!` no longer works, so we do not
+want the characteristic of `F` to be divisible by `d!`. As `Polynomial.hilbertPoly` may take
+any `p : F[X]` and `d : ℕ` as its inputs, it is necessary for us to assume that `CharZero F`.
+
+## Main definitions
+
+* `Polynomial.hilbertPoly p d`. Given a field `F`, a polynomial `p : F[X]` and a natural number `d`,
+  if `F` is of characteristic `0`, then `Polynomial.hilbertPoly p d : F[X]` is the polynomial whose
+  value at `n` equals the coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+
+## TODO
+
+* Hilbert polynomials of finitely generated graded modules over Noetherian rings.
+-/
+
+open Nat PowerSeries
+
+variable (F : Type*) [Field F]
+
+namespace Polynomial
+
+/--
+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`.
+-/
+noncomputable def preHilbertPoly (d k : ℕ) : F[X] :=
+  (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (Polynomial.X - (C (k : F)) + 1))
+
+lemma preHilbertPoly_eq_choose_sub_add [CharZero F] (d : ℕ) {k n : ℕ} (hkn : k ≤ n):
+    (preHilbertPoly F d k).eval (n : F) = (n - k + d).choose d := by
+  have : ((d ! : ℕ) : F) ≠ 0 := by norm_cast; positivity
+  calc
+  _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
+  _ = (n - k + d).choose d := by
+    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
+    field_simp [ascFactorial_eq_factorial_mul_choose]
+
+variable {F}
+
+/--
+`Polynomial.hilbertPoly p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbertPoly p (d + 1)`
+is defined as `∑ i in p.support, (p.coeff i) • Polynomial.preHilbertPoly F d i`. If
+`M` is a graded module whose Poincaré series can be written as `p(X)/(1 - X)ᵈ` for some
+`p : ℚ[X]` with integer coefficients, then `Polynomial.hilbertPoly p d` is the Hilbert
+polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval`,
+which says that `PowerSeries.coeff F n (p * (PowerSeries.invOneSubPow F d))` equals
+`(Polynomial.hilbertPoly p d).eval (n : F)` for any large enough `n : ℕ`.
+-/
+noncomputable def hilbertPoly (p : F[X]) : (d : ℕ) → F[X]
+  | 0 => 0
+  | d + 1 => ∑ i in p.support, (p.coeff i) • preHilbertPoly F d i
+
+variable (F) in
+lemma hilbertPoly_zero_nat (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]
+
+lemma hilbertPoly_poly_zero (p : F[X]) : hilbertPoly p 0 = 0 := rfl
+
+lemma hilbertPoly_poly_succ (p : F[X]) (d : ℕ) :
+    hilbertPoly p (d + 1) = ∑ i in p.support, (p.coeff i) • preHilbertPoly F d i := rfl
+
+variable (F) in
+lemma hilbertPoly_X_pow_succ (d k : ℕ) :
+    hilbertPoly ((X : F[X]) ^ k) (d + 1) = preHilbertPoly F d k := by
+  delta hilbertPoly; simp
+
+/--
+The key property of Hilbert polynomials. If `F` is a field with characteristic `0`, `p : F[X]` and
+`d : ℕ`, then for any large enough `n : ℕ`, `(Polynomial.hilbertPoly p d).eval (n : F)` equals the
+coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+-/
+theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval
+    [CharZero F] {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) :
+    PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbertPoly p d).eval (n : F) := by
+  delta hilbertPoly; induction d with
+  | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
+            exact coeff_eq_zero_of_natDegree_lt hn
+  | succ d hd =>
+      simp only [eval_finset_sum, eval_smul, smul_eq_mul]
+      rw [← Finset.sum_coe_sort]
+      have h_le (i : p.support) : (i : ℕ) ≤ n :=
+        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
+      have h (i : p.support) : eval ↑n (preHilbertPoly F d ↑i) = (n + d - ↑i).choose d := by
+        rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]
+      simp_rw [h]
+      rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _),
+        PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk,
+        invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)]
+      simp only [coeff_coe, coeff_mk]
+      symm
+      refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
+      · rw [Finset.mem_range_succ_iff]
+        exact h_le ⟨s, hs⟩
+      · simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
+        rw [hx.2, zero_mul]
+      · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
+
+end Polynomial
diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
index d6872afb27cbc..29176297e9018 100644
--- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean
+++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean
@@ -153,10 +153,20 @@ theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
     rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
       eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
 
+theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type*) [Semiring S] (n k : ℕ) :
+    (ascPochhammer S k).eval (n : S) = n.ascFactorial k := by
+  norm_cast
+  rw [ascPochhammer_nat_eq_ascFactorial]
+
 theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
     (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
   rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']
 
+theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type*) [Semiring S] (a b : ℕ) :
+    (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b := by
+  norm_cast
+  rw [ascPochhammer_nat_eq_descFactorial]
+
 @[simp]
 theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
     (ascPochhammer S n).natDegree = n := by
diff --git a/Mathlib/RingTheory/PowerSeries/WellKnown.lean b/Mathlib/RingTheory/PowerSeries/WellKnown.lean
index ef67977a0a5d2..ca5bd0b442330 100644
--- a/Mathlib/RingTheory/PowerSeries/WellKnown.lean
+++ b/Mathlib/RingTheory/PowerSeries/WellKnown.lean
@@ -151,10 +151,9 @@ theorem invOneSubPow_inv_eq_one_sub_pow :
   | zero => exact Eq.symm <| pow_zero _
   | succ d => rfl
 
-theorem invOneSubPow_inv_eq_one_of_eq_zero (h : d = 0) :
-    (invOneSubPow S d).inv = 1 := by
+theorem invOneSubPow_inv_zero_eq_one : (invOneSubPow S 0).inv = 1 := by
   delta invOneSubPow
-  simp only [h, Units.inv_eq_val_inv, inv_one, Units.val_one]
+  simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]
 
 theorem mk_add_choose_mul_one_sub_pow_eq_one :
     (mk fun n ↦ Nat.choose (d + n) d : S⟦X⟧) * ((1 - X) ^ (d + 1)) = 1 :=