pow_card — Mathlib

English

Let K be a finite field of size q. Then for every a ∈ K, a^q = a.

Русский

Пусть K — конечное поле размером q. Тогда для каждого a ∈ K выполняется a^q = a.

LaTeX

$$$a^q = a$ for all $a \in K$$$

Lean4

theorem pow_card (a : K) : a ^ q = a := by
  by_cases h : a = 0; · rw [h]; apply zero_pow Fintype.card_ne_zero
  rw [← Nat.succ_pred_eq_of_pos Fintype.card_pos, pow_succ, Nat.pred_eq_sub_one, pow_card_sub_one_eq_one a h, one_mul]

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