∀ {R : Type u_6} [inst : CommSemiring R] {S : Type u_7} [inst_1 : CommSemiring S] {K : Type u_8}
  [inst_2 : CommSemiring K] [inst_3 : Algebra R K] (e : R ≃+* S) [inst_4 : Algebra S K],
  (∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)) → ∀ [IsFractionRing S K], IsFractionRing R K