Commit 2026-03-21 08:07 c535a0f8
View on Github →feat: trivial lemmas and simp lemmas concerning iteratedFDeriv and taylorSeries (#36214)
To prepare for upcoming PRs, add several trivial lemmas and simp lemmas concerning iteratedFDeriv and taylorSeries. Use @[to_fun] to port several existing statements to match new style conventions.