pow_card — Mathlib

English

For all K, p, n with p prime and CharP K p, if q = p^n, then frobenius K p^n = 1 on K.

Русский

Для поля K и простого p с q = p^n, Frobenius^n равно тождественному отображению на K.

LaTeX

$$$\\forall {p} {n}, \\ {q = p^n} \\Rightarrow (\\operatorname{frobenius} K p)^n = 1$$$

Lean4

/-- A variation on Fermat's little theorem. See `ZMod.pow_card_sub_one_eq_one` -/
@[simp]
theorem pow_card (x : ZMod p) : x ^ p = x := by have h := FiniteField.pow_card x; rwa [ZMod.card p] at h

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