addChar_of_value_at_one_def — Mathlib

English

For every r with hr, the additive character satisfies addChar_of_value_at_one r hr (1) = 1 + r.

Русский

Для каждого r с hr выполняется addChar_of_value_at_one r hr (1) = 1 + r.

LaTeX

$$$$\operatorname{addChar\_of\_value\_at\_one}(r,hr)(1)=1+r.$$$$

Lean4

@[simp]
theorem addChar_of_value_at_one_def {r : R} (hr : Tendsto (r ^ ·) atTop (𝓝 0)) :
    addChar_of_value_at_one r hr (1 : ℤ_[p]) = 1 + r :=
  by
  change mahlerSeries (r ^ ·) ↑(1 : ℕ) = _
  rw [mahlerSeries_apply_nat hr le_rfl, Finset.sum_range_succ, Finset.sum_range_one, Nat.choose_zero_right,
    Nat.choose_self, one_smul, one_smul, pow_zero, pow_one]

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