Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_strict_deriv_at.real_of_complex

Modification history

2021-02-14 16:06
src/analysis/complex/real_deriv.lean
feat(analysis/special_functions): strict differentiability of some functions (#6228)
Added has_strict_deriv_at.real_of_complexView on Github →