Def expSeries

Modification history

2023-11-17 14:37

Mathlib/Analysis/NormedSpace/Exponential.lean

chore: exp -> NormedSpace.exp (#8436) …

Deleted expSeries View on Github →

2023-06-02 10:22

Mathlib/Analysis/NormedSpace/Exponential.lean

feat: port Analysis.NormedSpace.Exponential (#4567)

Added expSeries View on Github →