unit_norm_eq_one — Mathlib

English

The norm of χ(a) is 1 for any unit a in (ZMod n)×, i.e., ‖χ(a)‖ = 1.

Русский

Норма значения χ(a) равна 1 для любой единицы a в (ZMod n)×, т.е. ‖χ(a)‖ = 1.

LaTeX

$$$\\forall a \\in (\\mathbb{Z}/n\\mathbb{Z})^{\\times},\\; \\|χ(a)\\| = 1.$$$

Lean4

/-- The value at a unit of a Dirichlet character with target a normed field has norm `1`. -/
@[simp]
theorem unit_norm_eq_one (a : (ZMod n)ˣ) : ‖χ a‖ = 1 :=
  by
  refine (pow_eq_one_iff_of_nonneg (norm_nonneg _) (Nat.card_pos (α := (ZMod n)ˣ)).ne').mp ?_
  rw [← norm_pow, ← map_pow, ← Units.val_pow_eq_pow_val, pow_card_eq_one', Units.val_one, map_one, norm_one]

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