English
Let F be a finite field and R a commutative ring that contains a primitive (|F×|)-th root of unity. Then there exists a multiplicative character χ on F whose order is exactly |F×| = |F|−1.
Русский
Пусть F — конечное поле, а R — коммутативное кольцо, содержащее примитивный корень единстве́н (порядка |F×|). Тогда существует мультипликативный характер χ на F such that порядок χ равен |F×| = |F|−1.
LaTeX
$$$\exists \chi : \mathrm{MulChar}(F,R),\ \operatorname{order}(\chi) = |F^{\times}|$$$
Lean4
/-- There is always a character on `F` of order `#F-1` with values in a ring that has
a primitive `(#F-1)`th root of unity. -/
theorem exists_mulChar_orderOf_eq_card_units [DecidableEq F] {ζ : R} (hζ : IsPrimitiveRoot ζ (Fintype.card Fˣ)) :
∃ χ : MulChar F R, orderOf χ = Fintype.card Fˣ :=
exists_mulChar_orderOf F (by rw [Fintype.card_units]) hζ
