English
There exists a multiplicative character χ on a finite field F with order n provided n | (|F| - 1) and a primitive nth root of unity in R.
Русский
Существует мультисимвол χ на поле F с порядком n, если n делит |F| - 1 и в R есть примитивный корень единицы порядка n.
LaTeX
$$∃ χ : MulChar F R, orderOf χ = n$$
Lean4
/-- There is a character of order `n` on `F` if `#F ≡ 1 mod n` and the target contains
a primitive `n`th root of unity. -/
theorem exists_mulChar_orderOf {n : ℕ} (h : n ∣ Fintype.card F - 1) {ζ : R} (hζ : IsPrimitiveRoot ζ n) :
∃ χ : MulChar F R, orderOf χ = n := by
classical
have hn₀ : 0 < n := by
refine Nat.pos_of_ne_zero fun hn ↦ ?_
simp only [hn, zero_dvd_iff, Nat.sub_eq_zero_iff_le] at h
exact (Fintype.one_lt_card.trans_le h).false
let e := MulChar.equiv_rootsOfUnity F R
let ζ' : Rˣ := (hζ.isUnit hn₀.ne').unit
have h' : ζ' ^ (Fintype.card Fˣ : ℕ) = 1 :=
Units.ext_iff.mpr <| (hζ.pow_eq_one_iff_dvd _).mpr <| Fintype.card_units (α := F) ▸ h
use e.symm ⟨ζ', (mem_rootsOfUnity (Fintype.card Fˣ) ζ').mpr h'⟩
rw [e.symm.orderOf_eq, orderOf_eq_iff hn₀]
refine ⟨?_, fun m hm hm₀ h ↦ ?_⟩
· ext
push_cast
exact hζ.pow_eq_one
· rw [Subtype.ext_iff, Units.ext_iff] at h
push_cast at h
exact ((Nat.le_of_dvd hm₀ <| hζ.dvd_of_pow_eq_one _ h).trans_lt hm).false
