algebraMap_exp_comm — Mathlib

English

If a normed ring A is a normed algebra over two fields, the expSeries defined using each field coincide on A.

Русский

Если нормированное кольцо A является нормированной алгеброй над двумя полями, то экспонентные серии, определённые над каждым полем, совпадают на A.

LaTeX

$$$\\expSeries 𝕂 𝔸 n \\;\\text{and}\\; \\expSeries 𝕂' 𝔸 n \\text{ agree on } x$$$

Lean4

theorem algebraMap_exp_comm (x : 𝕂) : algebraMap 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebraMap 𝕂 𝔸 x) :=
  algebraMap_exp_comm_of_mem_ball x <| (expSeries_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _

Похожие утверждения