basic): add `times_cont_diff.real_of_complex` (#5073)

Commit

5 years ago

chore(analysis/complex/basic): add `times_cont_diff.real_of_complex` (#5073) Also rename `has_deriv_at_real_of_complex` to `has_deriv_at.real_of_complex`.

Author

urkud

Parents

87439b98

mathlib3 a6498516 - chore(analysis/complex/basic): add `times_cont_diff.real_of_complex` (#5073)

mathlib3
a6498516 - chore(analysis/complex/basic): add `times_cont_diff.real_of_complex` (#5073)