frobenius_zmodp — Mathlib

English

Let p be a prime and x any Witt vector over Z/pZ. The Frobenius endomorphism fixes x; i.e., frobenius x = x.

Русский

Пусть p — простое число и x — произвольный Witt-вектор над Z/pZ. Операция Фробениуса действует как тождество: frobenius x = x.

LaTeX

$$$\forall x \in \mathrm{WittVector}_p\big(\mathbb{Z}/p\mathbb{Z}\big),\; \operatorname{frobenius}(x) = x$$$

Lean4

@[simp]
theorem frobenius_zmodp (x : 𝕎 (ZMod p)) : frobenius x = x := by
  simp only [WittVector.ext_iff, coeff_frobenius_charP, ZMod.pow_card, forall_const]

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