Theorem PowerSeries.invOneSubPow_add

Modification history

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.invOneSubPow_add View on Github →