2024-12-04 20:23
Mathlib/RingTheory/PowerSeries/WellKnown.lean
feat(RingTheory/Polynomial/Hilbert): `Polynomial.exists_unique_hilbertPoly` and `Polynomial.hilbertPoly_mul_one_sub_pow_add` (#19404)
Added PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow