Theorems · Theorem · number theory

MulChar.exists_mulChar_orderOf

∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] {R : Type u_2} [inst_2 : CommRing R] {n : ℕ},
  n ∣ Fintype.card F - 1 → ∀ {ζ : R}, IsPrimitiveRoot ζ n → ∃ χ, orderOf χ = n

There is a character of order n on F if #F ≡ 1 mod n and the target contains a primitive nth root of unity.

Defined in

Mathlib.NumberTheory.MulChar.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeCommRing