Theorems · Theorem · functional analysis

NormedSpace.expSeries_eq_expSeries

∀ (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [inst : Field 𝕂] [inst_1 : Field 𝕂'] [inst_2 : Ring 𝔸]
  [inst_3 : Algebra 𝕂 𝔸] [inst_4 : Algebra 𝕂' 𝔸] [inst_5 : TopologicalSpace 𝔸] [inst_6 : IsTopologicalRing 𝔸] (n : ℕ)
  (x : 𝔸), ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (NormedSpace.expSeries 𝕂' 𝔸 n) fun x_1 => x

If a normed ring 𝔸 is a normed algebra over two fields, then they define the same expSeries on 𝔸.

Defined in

Mathlib.Analysis.Normed.Algebra.Exponential

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldRingAlgebraAlgebraTopologicalSpaceIsTopologicalRing