frobenius_pow — Mathlib

English

If |K| = p^n, then the nth power of Frobenius equals the identity on K.

Русский

Пусть |K| = p^n; тогда n-ая степень Фробениуса является тождественным отображением на K.

LaTeX

$$$\\operatorname{frobenius}_{K,p}^{\,n} = \\operatorname{id}_K \\quad\\text{whenever } |K| = p^n$$$

Lean4

theorem frobenius_pow {p : ℕ} [Fact p.Prime] [CharP K p] {n : ℕ} (hcard : q = p ^ n) : frobenius K p ^ n = 1 :=
  by
  ext x; conv_rhs => rw [RingHom.one_def, RingHom.id_apply, ← pow_card x, hcard]
  clear hcard
  induction n with
  | zero => simp
  | succ n hn => rw [pow_succ', pow_succ, pow_mul, RingHom.mul_def, RingHom.comp_apply, frobenius_def, hn]

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