frobenius — Mathlib

English

The Frobenius automorphism of the base field induces an automorphism of the Witt fraction field; equivalently, Frobenius extends to an automorphism of the fraction field of Witt vectors.

Русский

Фробениус-автоморфизм базы поля порождает автоморфизм поля дробей относительных Witt-векторов; другими словами, Фробениус растягивается до автоморфизма дробей Witt.

LaTeX

$$$\text{The Frobenius on } k \text{ induces an automorphism } K(p,k) \to K(p,k).$$$

Lean4

/-- The Frobenius automorphism of `k` induces an automorphism of `K`. -/
def frobenius : K(p, k) ≃+* K(p, k) :=
  IsFractionRing.ringEquivOfRingEquiv (frobeniusEquiv p k)

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