∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p],
  RingHomInvPair ↑(WittVector.FractionRing.frobenius p k).symm ↑(WittVector.FractionRing.frobenius p k)