Commit 2023-11-02 19:35 43964826

View on Github →

feat: add some missing PowerSeries.coeff_C lemmas (#8019) These parallel the lemmas for Polynomial

Estimated changes

Modified Mathlib/RingTheory/HahnSeries.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem PowerSeries.coeff_ne_zero_C

added theorem PowerSeries.coeff_succ_C

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean