Theorems · Theorem · number theory

DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity

∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [Nontrivial R] ⦃a : ZMod n⦄, a ≠ 1 → ∃ χ, χ a ≠ 1

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.

Defined in

Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Cited by

1 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingNeZeroHasEnoughRootsOfUnityNontrivial