Theorem contDiffWithinAt_fun_id

Modification history

2026-05-17 17:16
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
feat(Tactic/ToFun): allow configuring the name of the generated declaration (#34257) …
Deleted contDiffWithinAt_fun_idView on Github →
2025-05-13 11:52
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
feat: fun_prop for ContDiff (#24056) …
Added contDiffWithinAt_fun_idView on Github →