Commit 2024-12-04 20:23 7a05b449

View on Github →

feat(RingTheory/Polynomial/Hilbert): Polynomial.exists_unique_hilbertPoly and Polynomial.hilbertPoly_mul_one_sub_pow_add (#19404)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

added theorem Polynomial.exists_unique_hilbertPoly

added theorem Polynomial.hilbertPoly_mul_one_sub_pow_add

added theorem Polynomial.hilbertPoly_mul_one_sub_succ

Modified Mathlib/RingTheory/PowerSeries/WellKnown.lean

added theorem PowerSeries.invOneSubPow_add

added theorem PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow

added theorem PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val