Commit 2025-02-15 04:27 5d264f35

View on Github →

chore(Analysis): relax arguments of iteratedFDerivWithin_add_apply and friends (#21677)

Estimated changes

Modified Mathlib/Analysis/Analytic/IteratedFDeriv.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

modified theorem iteratedFDerivWithin_add_apply'

modified theorem iteratedFDerivWithin_add_apply

modified theorem iteratedFDeriv_add_apply'

modified theorem iteratedFDeriv_add_apply

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

modified theorem iteratedDerivWithin_add

modified theorem iteratedDerivWithin_sub

modified theorem iteratedDeriv_add

modified theorem iteratedDeriv_sub

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean