Theorem iteratedDeriv_mul

Modification history

2026-01-29 18:03

Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

feat(Analysis/Analytic, Analysis/Calculus): allow more general types in SMul (#34515) …

Modified iteratedDeriv_mul View on Github →

2026-01-13 15:36

Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃` (#33723)

Added iteratedDeriv_mul View on Github →