Theorem Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval

Modification history

2024-12-02 18:04

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

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) …

Added Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval View on Github →