DirichletCharacter.unit_norm_eq_one
theorem DirichletCharacter.unit_norm_eq_one :
∀ {F : Type u_1} [inst : NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : (ZMod n)ˣ), ‖χ ↑a‖ = 1
This theorem states that for any normed field `F`, a natural number `n`, a Dirichlet character `χ` of level `n` with target field `F`, and a unit `a` of the integers modulo `n`, the norm of the value of `χ` at `a` is equal to `1`. In other words, if `χ` is a Dirichlet character mapping values from the ring of integers modulo `n` to the field `F`, then the magnitude of the value `χ(a)` is `1` when `a` is a unit in the integer modulo algebra, according to the norm defined on `F`.
More concisely: For any Dirichlet character χ of level n and target field F over a normed field F, the norm of χ(a) is equal to 1 when a is a unit in the integers modulo n.
|
DirichletCharacter.norm_le_one
theorem DirichletCharacter.norm_le_one :
∀ {F : Type u_1} [inst : NormedField F] {n : ℕ} (χ : DirichletCharacter F n) (a : ZMod n), ‖χ a‖ ≤ 1
The theorem `DirichletCharacter.norm_le_one` states that for any normed field `F`, any positive integer `n`, any Dirichlet character `χ` on `F` of level `n`, and any integer `a` modulo `n`, the norm of the value of `χ` at `a` is less than or equal to 1. In other words, the values of a Dirichlet character, when mapped to a normed field, have their norms bounded by 1.
More concisely: For any Dirichlet character χ of level n on a normed field F, |χ(a)| ≤ 1 for all integers a modulo n.
|