mathlib3

7459c21c - feat(analysis/special_functions): strict differentiability of `real.exp` and `real.log` (#6256)