Theorems · Definition · functional analysis

NormedSpace.exp

{𝔸 : Type u_3} → [inst : Ring 𝔸] → [inst_1 : TopologicalSpace 𝔸] → [IsTopologicalRing 𝔸] → 𝔸 → 𝔸

NormedSpace.exp : 𝔸 → 𝔸 is the exponential map. It is defined as the sum of the FormalMultilinearSeries expSeries ℚ 𝔸. If 𝔸 can't be equipped with a ℚ-algebra structure, we use the junk value 1. For details on why this approach is taken, see the module documentation for Mathlib/Analysis/Normed/Algebra/Exponential.lean. Note that when 𝔸 = Matrix n n 𝕂, this is the Matrix Exponential; see Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean for lemmas specific to that case.

Defined in

Mathlib.Analysis.Normed.Algebra.Exponential

Cited by

157 results in Mathlib

Foundations

Depth 83 from the axioms, rests on 2,007 definitions · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpaceIsTopologicalRing