Theorem HasDerivAt.of_real_comp

Modification history

2023-06-10 02:10

Mathlib/Analysis/Complex/RealDeriv.lean

chore: use `ofReal` instead of `of_real` in lemma names (#4934)

Deleted HasDerivAt.of_real_comp View on Github →

2023-06-04 13:34

Mathlib/Analysis/Complex/RealDeriv.lean

feat: port Analysis.Complex.RealDeriv (#4642)

Added HasDerivAt.of_real_comp View on Github →