Theorems · Definition · number theory

WittVector.FractionRing.frobenius

(p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        [CharP k p] → [PerfectRing k p] → FractionRing (WittVector p k) ≃+* FractionRing (WittVector p k)

The Frobenius automorphism of k induces an automorphism of K.

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

9 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FactCommRingCharPPerfectRing