Theorem ContDiffWithinAt.differentiableWithinAt'

Modification history

2025-12-22 11:55

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

refactor(Analysis,Geometry): assume `n ≠ 0`, not `1 ≤ n` (#33131) …

Modified ContDiffWithinAt.differentiableWithinAt'View on Github →

2024-10-10 16:56

Mathlib/Analysis/Calculus/ContDiff/Defs.lean

chore: rename leftovers from the port (#17619)

Added ContDiffWithinAt.differentiableWithinAt'View on Github →