Def Complex.exp

Modification history

2025-12-08 21:44

Mathlib/Analysis/Complex/Exponential.lean

perf(Analysis.Complex.Exponential): make `Complex.exp` an `irreducible_def` (#32599) …

Deleted Complex.exp View on Github →

2023-03-15 16:55

Mathlib/Data/Complex/Exponential.lean

feat: port Data.Complex.Exponential (#2785)

Added Complex.exp View on Github →