Theorem exp_sum

Modification history

2023-11-17 14:37

Mathlib/Analysis/NormedSpace/Exponential.lean

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

Deleted exp_sum View on Github →

2023-06-02 10:22

Mathlib/Analysis/NormedSpace/Exponential.lean

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

Added exp_sum View on Github →