orderOf_dvd_card_sub_one — Mathlib

English

The order of a character χ divides |F| - 1 when χ has order n on a finite field F.

Русский

Порядок χ делит |F| - 1, когда χ имеет порядок n на конечном поле F.

LaTeX

$$orderOf χ ∣ Fintype.card F - 1$$

Lean4

/-- If there is a multiplicative character of order `n` on `F`, then `#F ≡ 1 mod n`. -/
theorem orderOf_dvd_card_sub_one (χ : MulChar F R) : orderOf χ ∣ Fintype.card F - 1 := by
  classical
  rw [← Fintype.card_units]
  exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Похожие утверждения