tsum_coe — Mathlib

English

The sum of a real-valued series, when embedded into ℍ via the canonical embedding, equals the quaternion embedding of the real sum.

Русский

Сумма вещественного ряда после вложения в ℍ равна вложению суммы в ℍ.

LaTeX

$$$\operatorname{tsum}_{L}(\lambda a, (f a)) = \operatorname{Quaternion.coe}(\operatorname{tsum}_{L} f)$$$

Lean4

@[norm_cast]
theorem tsum_coe (f : α → ℝ) : (∑'[L] a, (f a : ℍ)) = ↑(∑'[L] a, f a) :=
  (Function.LeftInverse.map_tsum f (continuous_algebraMap _ _) continuous_re re_coe).symm

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