Commit 2025-05-13 18:00 440abb3d

View on Github →

chore: whitespace adaptations (#24854) Found by #24465.

Estimated changes

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

modified theorem ContDiff.deriv'

modified theorem ContDiff.iteratedFDeriv_right'

modified theorem ContDiffAt.fderiv_right_succ

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

modified theorem ContDiff.differentiable_iteratedDeriv'