coe_addChar_of_value_at_one — Mathlib

English

For all r with Tendsto (r^·) atTop to 0, the additive character addChar_of_value_at_one r hr equals the Mahler series mahlerSeries(r^·).

Русский

Для всех r, для которых r^n → 0, аддитивный характер addChar_of_value_at_one r hr совпадает с рядом Махлера mahlerSeries(r^·).

LaTeX

$$$$\operatorname{addChar\_of\_value\_at\_one}(r,hr)=\operatorname{mahlerSeries}(r^{\cdot}).$$$$

Lean4

theorem coe_addChar_of_value_at_one {r : R} (hr : Tendsto (r ^ ·) atTop (𝓝 0)) :
    (addChar_of_value_at_one r hr : ℤ_[p] → R) = mahlerSeries (r ^ ·) :=
  rfl

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