Theorem differentiableOn_finCons'

Modification history

2026-09-09 09:50
Mathlib/Analysis/Calculus/FDeriv/Prod.lean
chore(Analysis/Calculus/FDeriv/Prod): deprecate differentiable*_finCons' as duplicates (#42583) …
Deleted differentiableOn_finCons'View on Github →
2025-01-29 23:20
Mathlib/Analysis/Calculus/FDeriv/Prod.lean
feat: `HasFDerivAt` for `Fin.cons` (#20407) …
Added differentiableOn_finCons'View on Github →