Theorem not_differentiableAt_abs_zero

Modification history

2023-12-09 12:32
Mathlib/Analysis/Calculus/Deriv/Add.lean
chore(*Deriv*): golf (#8899) …
Modified not_differentiableAt_abs_zeroView on Github →
2023-10-19 16:29
Mathlib/Analysis/InnerProductSpace/Calculus.lean
feat(Analysis/InnerProductSpace/Calculus): Add theorem that abs on ℝ is not differentiable at 0 (#7362) …
Added not_differentiableAt_abs_zeroView on Github →