pow_card_pow — Mathlib

English

For a finite field K and any n ∈ ℕ, the n-th iterate of Frobenius equals raising to the q^n power: a^{q^n} = a for all a ∈ K.

Русский

Для конечного поля K и любого n ∈ ℕ, n-й итерации Фробениуса эквивалентна возведению в степень q^n: a^{q^n} = a для всех a ∈ K.

LaTeX

$$$a^{q^n} = a$ for all $a \in K$$$

Lean4

theorem pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a := by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

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