modOne_eq_one — Mathlib

English

Dirichlet character modulo 1 is the constant-1 function; twisting yields the constant function 1.

Русский

Dirichlet-символ модуля 1 — константа, равная 1; поворот χ· даёт константу 1.

LaTeX

$$$(χ \cdot) = 1 \quad \text{для } χ : DirichletCharacter \mathbb{R} 1.$$$

Lean4

/-- The Dirichlet character mod `1` corresponds to the constant function `1`. -/
theorem modOne_eq_one {R : Type*} [CommMonoidWithZero R] {χ : DirichletCharacter R 1} : ((χ ·) : ℕ → R) = 1 :=
  by
  ext
  rw [χ.level_one, MulChar.one_apply (isUnit_of_subsingleton _), Pi.one_apply]

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