∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k],
  RingHomClass (FractionRing (WittVector p k) ≃+* FractionRing (WittVector p k)) (FractionRing (WittVector p k))
    (FractionRing (WittVector p k))