Theorem ContDiff.real_of_complex

Modification history

2024-11-25 11:42

Mathlib/Analysis/Complex/RealDeriv.lean

feat: extend `ContDiff` to take a smoothness exponent in `WithTop ℕ∞` (#19442) …

Modified ContDiff.real_of_complex View on Github →

2023-06-04 13:34

Mathlib/Analysis/Complex/RealDeriv.lean

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

Added ContDiff.real_of_complex View on Github →