Theorems · Theorem · group theory

CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity

∀ (G : Type u_1) (M : Type u_2) [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] {a : G}, a ≠ 1 → ∃ φ, φ a ≠ 1

If G is a finite commutative group of exponent n and M is a commutative monoid with enough nth roots of unity, then for each a ≠ 1 in G, there exists a group homomorphism φ : G → Mˣ such that φ a ≠ 1.

Defined in

Mathlib.GroupTheory.FiniteAbelian.Duality

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommGroupFiniteCommMonoidHasEnoughRootsOfUnity