Theorems · Definition · number theory

WittVector.Isocrystal.frob

{p : ℕ} →
  {inst : Fact (Nat.Prime p)} →
    {k : Type u_1} →
      {inst_1 : CommRing k} →
        {inst_2 : CharP k p} →
          {inst_3 : PerfectRing k p} →
            {V : Type u_2} →
              {inst_4 : AddCommGroup V} →
                [self : WittVector.Isocrystal p k V] → V ≃ₛₗ[WittVector.FractionRing.frobeniusRingHom p k] V

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

0 results in Mathlib

Foundations

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

Assumes

WittVector.Isocrystal