Theorem exp_zero

Modification history

2023-11-17 14:37

Mathlib/Analysis/NormedSpace/Exponential.lean

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

Deleted exp_zero View on Github →

2023-07-16 14:44

Mathlib/Analysis/NormedSpace/Exponential.lean

feat(Topology.Algebra.InfiniteSum): make sure that tsum and sum coincide on fintypes (#5914) …

Modified exp_zero View on Github →

2023-06-02 10:22

Mathlib/Analysis/NormedSpace/Exponential.lean

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

Added exp_zero View on Github →