Theorems · Theorem · number theory

MulChar.exists_apply_ne_one_of_hasEnoughRootsOfUnity

∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] [Nontrivial R] {a : M}, a ≠ 1 → ∃ χ, χ a ≠ 1

If M is a finite commutative monoid and R is a ring that has enough roots of unity, then for each a ≠ 1 in M, there exists a multiplicative character χ : M → R such that χ a ≠ 1.

Defined in

Mathlib.NumberTheory.MulChar.Duality

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidCommRingFiniteHasEnoughRootsOfUnityNontrivial