no goals
R : Type ?u.1246489
inst✝⁹ : CommRing R
S : Submonoid R
P : Type ?u.1246696
inst✝⁸ : CommRing P
inst✝⁷ : Algebra R P
loc : IsLocalization S P
R₁ : Type u_1
inst✝⁶ : CommRing R₁
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Algebra R₁ K
frac : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
I✝ J : FractionalIdeal R₁⁰ K
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (1 / I) = 1 / map (↑h) I
rw [map_div, map_one]