mathlib3
b0071f3f - feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255)

Commit

4 years ago

feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255) Also move lemmas about differentiability of `sqrt` out from `special_functions/pow` to a new file.

Author

urkud

Parents

8a431630

mathlib3 b0071f3f - feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255)

mathlib3
b0071f3f - feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255)