Theorem iteratedFDerivWithin_add_apply'

Modification history

2026-02-19 13:50

Mathlib/Analysis/Calculus/ContDiff/Operations.lean

feat: iterated derivatives of differences of functions (#35256) …

Deleted iteratedFDerivWithin_add_apply'View on Github →

2025-02-26 07:29

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

chore: split the long file `ContDiff.Basic` into two files (#22293)

Modified iteratedFDerivWithin_add_apply'View on Github →

2025-02-15 04:27

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

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

Modified iteratedFDerivWithin_add_apply'View on Github →

2023-06-04 09:37

Mathlib/Analysis/Calculus/ContDiff.lean

feat: port Analysis.Calculus.ContDiff (#4532)

Added iteratedFDerivWithin_add_apply'View on Github →