no goals
R : Type ?u.33955
A : Type ?u.33958
K : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Field K
inst✝⁷ : IsDomain A
R₁ : Type u_1
inst✝⁶ : CommRing R₁
inst✝⁵ : IsDomain R₁
inst✝⁴ : Algebra R₁ K
inst✝³ : IsFractionRing R₁ K
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) I⁻¹ = (map (↑h) I)⁻¹
rw [inv_eq, map_div, map_one, inv_eq]