frobenius_zmod — Mathlib

English

For prime p, Frobenius on ZMod p with p equals the identity map.

Русский

Для простого p отображение Фробениуса на ZMod p совпадает с тождественным отображением.

LaTeX

$$$\\operatorname{frobenius}(\\mathbb{Z}/p\\mathbb{Z}, p) = \\operatorname{id}_{\\mathbb{Z}/p\\mathbb{Z}}$$$

Lean4

@[simp]
theorem frobenius_zmod (p : ℕ) [Fact p.Prime] : frobenius (ZMod p) p = RingHom.id _ :=
  by
  ext a
  rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]
    -- This was a `simp` lemma, but now the LHS simplifies to `φ p`.

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