pow_card_sub_one_eq_one — Mathlib

English

For a finite field K, its cardinal q is a prime power; i.e., there exist a prime p and n ∈ ℕ⁺ with q = p^n.

Русский

Для конечного поля K кардинал q является простой степенью: существует простое p и положительное целое n, такие что q = p^n.

LaTeX

$$$\exists p \in \mathbb{N}, \; \text{Nat.Prime } p \land \exists n \in \mathbb{N}_{>0},\; q = p^{n}$$$

Lean4

theorem pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1 := by
  calc
    a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
      rw [Units.val_pow_eq_pow_val, Units.val_mk0]
    _ = 1 := by
      classical
      rw [← Fintype.card_units, pow_card_eq_one]
      rfl

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