no goals
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
p q : K[X]
hq : q ≠ 0
⊢ RatFunc.mk p q = { toFractionRing := Localization.mk p { val := q, property := (_ : q ∈ K[X]⁰) } }
rw [mk_def_of_ne, Localization.mk_eq_mk'] <;> exact hq