Commit 2026-11-10 23:38 16956b2a

View on Github →

feat(PowerSeries/Derivative): add some lemmas (#43305) In this PR, I migrated some results from Polynomial/Derivative.lean to PowerSeries/Derivative.lean.

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

added theorem PowerSeries.derivative_C_mul_X

added theorem PowerSeries.derivative_C_mul_X_pow

added theorem PowerSeries.derivative_C_mul_X_sq

added theorem PowerSeries.derivative_X_add_C

added theorem PowerSeries.derivative_X_pow

added theorem PowerSeries.derivative_X_pow_succ

added theorem PowerSeries.derivative_X_sq

added theorem PowerSeries.derivative_monomial

added theorem PowerSeries.derivative_monomial_succ

added theorem PowerSeries.iterate_derivative_smul

added theorem PowerSeries.iterate_derivative_sum

added theorem PowerSeries.iterate_derivative_zero