English
Let 𝔸 be a normed algebra over two fields 𝕂 and 𝕂'. If both structures turn 𝔸 into a normed algebra over their respective fields, then the exponential maps determined by 𝕂 and by 𝕂' coincide; i.e. exp_𝕂 = exp_𝕂' as functions 𝔸 → 𝔸.
Русский
Пусть 𝔸 — нормированная алгебра над двумя полями 𝕂 и 𝕂'. Если структура сделает 𝔸 нормированной алгеброй над каждым полем, то экспоненциальные функции, определяемые 𝕂 и 𝕂', совпадают: exp_𝕂 = exp_𝕂' как отображения 𝔸 → 𝔸.
LaTeX
$$$\\exp_{\\mathbb{K}} = \\exp_{\\mathbb{K}'}$ as maps $A \\to A$.$$
Lean4
/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
exponential function on `𝔸`. -/
theorem exp_eq_exp : (exp 𝕂 : 𝔸 → 𝔸) = exp 𝕂' := by
ext x
rw [exp, exp]
refine tsum_congr fun n => ?_
rw [expSeries_eq_expSeries 𝕂 𝕂' 𝔸 n x]
