no goals
R : Type ?u.450373
inst✝⁵ : CommRing R
M : Submonoid R
S : Type ?u.450565
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P : Type ?u.450802
inst✝² : CommRing P
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
K : Type ?u.450982
r : A
s : { x // x ∈ nonZeroDivisors A }
⊢ Localization.mk r s = ↑(algebraMap A (FractionRing A)) r / ↑(algebraMap A (FractionRing A)) ↑s
rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]