Bounds for values of Dirichlet characters

We consider Dirichlet characters χ with values in a normed field F.

We show that ‖χ a‖ = 1 if a is a unit and ‖χ a‖ ≤ 1 in general.

@[simp]

theorem DirichletCharacter.unit_norm_eq_one {F : Type u_1} [NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : (ZMod n)ˣ) : ‖χ ↑a‖ = 1

The value at a unit of a Dirichlet character with target a normed field has norm 1.

theorem DirichletCharacter.norm_le_one {F : Type u_1} [NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : ZMod n) : ‖χ a‖ ≤ 1

The values of a Dirichlet character with target a normed field have norm bounded by 1.