frobeniusRingHom — Mathlib

English

The Frobenius map on Witt vectors induces a ring homomorphism on the corresponding fraction Ring.

Русский

Фробениус на Witt-векторах индуцирует кольцевой гомоморфизм на соответствующем дробовом кольце.

LaTeX

$$$\text{The map } frobeniusRingHom : K(p,k) \to K(p,k) \text{ is a ring homomorphism.}$$$

Lean4

/-- The Frobenius automorphism of `k` induces an endomorphism of `K`. For notation purposes.
Notation `φ(p, k)` in the `Isocrystal` namespace. -/
def frobeniusRingHom : K(p, k) →+* K(p, k) :=
  FractionRing.frobenius p k

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