Commit 2026-02-08 21:44 019f8537

View on Github →

feat(RingTheory/PowerSeries/Derivative): more lemmas (#34616) Four lemmas leading to the chain rule for power series.

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Derivative.lean

added theorem PowerSeries.derivative_pow

added theorem PowerSeries.derivative_subst

Modified Mathlib/RingTheory/PowerSeries/Substitution.lean

added theorem PowerSeries.HasSubst.eventually_coeff_pow_eq_zero