Exponential

DefinitionMatrix exponential#

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.

NormedSpace.exp.{u_2} {𝔸 : Type u_2} [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] (x : 𝔸) : 𝔸

Sources

• Mathlib documentation: NormedSpace.exp
• Source of NormedSpace.exp in Mathlib/Analysis/Normed/Algebra/Exponential.lean
• Mathlib undergraduate list: Linear algebra › Exponential

MathlibNormedSpace.exp

Uses 5 · Used by 2

Statement usesAssociative algebra over a commutative ring · Field \(\Q\) of rational numbers · Infinite sum · Multilinear map · Topological ring

Used byCos (power series expansion of elementary functions) · Sin (power series expansion of elementary functions)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.