Commit 2024-12-02 18:04 561e0504

feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of Polynomial.hilbertPoly p d for p : F[X] and d : ℕ, where F is a field. (#19303) Given any field F, polynomial p : F[X] and natural number d, we have defined Polynomial.hilbertPoly p d : F[X]. If F is of characteristic zero, then for any large enough n : ℕ, PowerSeries.coeff F n (p * (invOneSubPow F d)) equals (hilbertPoly p d).eval (n : F) (see Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval).