feat(RingTheory/Polynomial/Hilbert): Polynomial.exists_unique_hilbertPoly
and Polynomial.hilbertPoly_mul_one_sub_pow_add
#19404
+70
−4