Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 11:38 d43a3bae

View on Github →

feat(analysis/normed_space/inner_product): norm is smooth at x ≠ 0 (#6275)

Estimated changes

added theorem differentiable.dist
added theorem differentiable.norm
added theorem differentiable_at.dist
added theorem differentiable_at.norm
added theorem differentiable_on.dist
added theorem differentiable_on.norm
added theorem times_cont_diff.dist
added theorem times_cont_diff.norm