apply_eq_toArithmeticFunction_apply

English

For a Dirichlet character χ modulo N and any n ≠ 0, χ(n) equals the arithmetic-function twist evaluated at n: χ(n) = toArithmeticFunction(χ ·)(n).

Русский

Пусть χ — Dirichlet-символ модуля N; тогда при любом n ≠ 0 имеем χ(n) = toArithmeticFunction(χ ·)(n).

LaTeX

$$$\chi(n) = (\text{toArithmeticFunction}(χ \cdot))(n) \quad \text{при } n \neq 0.$$$

Lean4

theorem apply_eq_toArithmeticFunction_apply {N : ℕ} {R : Type*} [CommMonoidWithZero R] (χ : DirichletCharacter R N)
    {n : ℕ} (hn : n ≠ 0) : χ n = toArithmeticFunction (χ ·) n := by simp [toArithmeticFunction, hn]

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