expSeries_eq_expSeries — Mathlib

English

For a pair (A,B) with A,B Banach algebras, the second component of exp on A×B equals exp on the second component.

Русский

Для пары (A,B) экспонента на произведении имеет вторую компоненту равной экспоненте от второй компоненты.

LaTeX

$$$(\\exp 𝕂 x).snd = \\exp 𝕂 x.snd$$

Lean4

/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
`expSeries` on `𝔸`. -/
theorem expSeries_eq_expSeries (n : ℕ) (x : 𝔸) : (expSeries 𝕂 𝔸 n fun _ => x) = expSeries 𝕂' 𝔸 n fun _ => x := by
  rw [expSeries_apply_eq, expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝕂']

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