Theorem NormedSpace.exp_eq_ofScalarsSum

Modification history

2026-01-06 16:13

Mathlib/Analysis/Normed/Algebra/Exponential.lean

refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` (#30706) …

Modified NormedSpace.exp_eq_ofScalarsSum View on Github →

2024-11-09 07:31

Mathlib/Analysis/Normed/Algebra/Exponential.lean

feat: improve the Analysis.Analytic.OfScalars API and implement it for geometric and exponential functions (#18407) …

Added NormedSpace.exp_eq_ofScalarsSum View on Github →