Theorem differentiableWithinAt_id'

Modification history

2026-05-17 17:16
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
feat(Tactic/ToFun): allow configuring the name of the generated declaration (#34257) …
Deleted differentiableWithinAt_id'View on Github →
2024-12-28 10:33
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
chore: rename iteratedDeriv_const_{smul,mul} (#20136)
Added differentiableWithinAt_id'View on Github →