const_one_eq_zeta — Mathlib

English

Let R be an additive monoid with one. For every natural number n > 0, the constant-1 sequence evaluated at n coincides with the zeta-twisted arithmetic function at n.

Русский

Пусть R — моноид с единицей, добавочный. Для каждого натурального числа n > 0 константная функция 1 на n совпадает с функцией ζ· на n.

LaTeX

$$$\forall n \in \mathbb{N},\ n > 0 \Rightarrow 1 = (\zeta \cdot)(n).$$$

Lean4

theorem const_one_eq_zeta {R : Type*} [AddMonoidWithOne R] {n : ℕ} (hn : n ≠ 0) : (1 : ℕ → R) n = (ζ ·) n := by
  simp [hn]

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