rootNumber_modOne — Mathlib

English

The root number of the unique Dirichlet character modulo 1 is 1.

Русский

Корень число для единственного символа по модулю 1 равен 1.

LaTeX

$$$\text{rootNumber}(\chi) = 1 \quad\text{для } \chi \in \text{DirichletCharacter}(\mathbb{C},1)$$$

Lean4

/-- The root number of the unique Dirichlet character modulo 1 is 1. -/
theorem rootNumber_modOne (χ : DirichletCharacter ℂ 1) : rootNumber χ = 1 := by
  simp [rootNumber, gaussSum, -univ_unique, ← singleton_eq_univ (1 : ZMod 1),
    (show stdAddChar (1 : ZMod 1) = 1 from AddChar.map_zero_eq_one _), (show χ.Even from map_one _)]

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