norm_le_one — Mathlib

English

For any a ∈ ZMod n, the norm of χ(a) is at most 1: ‖χ(a)‖ ≤ 1.

Русский

Для любого a ∈ ZMod n нормa χ(a) не превосходит единицы: ‖χ(a)‖ ≤ 1.

LaTeX

$$$\\forall a:\\, \\|χ(a)\\| \\le 1.$$$

Lean4

/-- The values of a Dirichlet character with target a normed field have norm bounded by `1`. -/
theorem norm_le_one (a : ZMod n) : ‖χ a‖ ≤ 1 := by
  by_cases h : IsUnit a
  · exact (χ.unit_norm_eq_one h.unit).le
  · rw [χ.map_nonunit h, norm_zero]
    exact zero_le_one

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