Theorems · Theorem · number theory

ZMod.exists_monoidHom_apply_ne_one

∀ {M : Type u_7} [inst : CommMonoid M] {n : ℕ} [NeZero n],
  (∃ ζ, IsPrimitiveRoot ζ n) → ∀ {a : ZMod n}, a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

If M is a commutative group that contains a primitive nth root of unity and a : ZMod n is nonzero, then there exists a group homomorphism φ from the additive group ZMod n to the multiplicative group Mˣ such that φ a ≠ 1.

Defined in

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidNeZero