Theorem HasDerivAt.comp_of_real

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.comp_of_real View on Github →

2023-06-04 13:34

Mathlib/Analysis/Complex/RealDeriv.lean

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

Added HasDerivAt.comp_of_real View on Github →