English
Let R be a commutative ring with unity that has enough roots of unity for modulus n. For every a in Z/nZ with a ≠ 1, there exists a Dirichlet character χ mod n with values in R such that χ(a) ≠ 1.
Русский
Пусть R — коммутативное кольцо с единицей, обладающее достаточным количеством корней корня единства для модуля n. Для любого a в Z/nZ, отличного от 1, существует Dirichlet‑символ χ mod n со значениями в R, такой что χ(a) ≠ 1.
LaTeX
$$$\forall R\ [CommRing\ R]\ {n : \mathbb{N}}\ [NeZero\ n]\ [HasEnoughRootsOfUnity\ R (Monoid.exponent (ZMod n)ˣ)]\ [Nontrivial\ R], \forall ⦃a : ZMod n⦄, a \neq 1 \Rightarrow \exists χ : DirichletCharacter R n, χ a \neq 1$$$
Lean4
/-- If `R` is a ring that has enough roots of unity and `n ≠ 0`, then for each
`a ≠ 1` in `ZMod n`, there exists a Dirichlet character `χ` mod `n` with values in `R`
such that `χ a ≠ 1`. -/
theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity [Nontrivial R] ⦃a : ZMod n⦄ (ha : a ≠ 1) :
∃ χ : DirichletCharacter R n, χ a ≠ 1 :=
MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity (ZMod n) R ha
