Theorems · Theorem · number theory

IsCyclic.exists_apply_ne_one

∀ {G : Type u_7} {G' : Type u_8} [inst : Group G] [IsCyclic G] [Finite G] [inst_3 : CommGroup G'],
  (∃ ζ, IsPrimitiveRoot ζ (Nat.card G)) → ∀ ⦃a : G⦄, a ≠ 1 → ∃ φ, φ a ≠ 1

If G is cyclic of order n and G' contains a primitive nth root of unity, then for each a : G with a ≠ 1 there is a homomorphism φ : G →* G' such that φ a ≠ 1.

Defined in

Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupIsCyclicFiniteCommGroup