Theorem iteratedDeriv_const_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_const_mulView on Github →
2025-01-29 22:18
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
feat: add new iteratedDeriv_const_smul/mul (#20288) …
Added iteratedDeriv_const_mulView on Github →
2024-12-28 10:33
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
chore: rename iteratedDeriv_const_{smul,mul} (#20136)
Deleted iteratedDeriv_const_mulView on Github →
2024-01-26 22:26
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
feat: iteratedDeriv_const_{s,}mul, iteratedDeriv_{c,}exp_const_mul (#9767) …
Added iteratedDeriv_const_mulView on Github →