R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : FractionalIdeal S P
⊢ ↑{ val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } = ↑I * ↑J
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : FractionalIdeal S P
⊢ ↑(I * J) = ↑I * ↑J
simp only [mul_def]
no goals
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
loc : IsLocalization S P
I J : FractionalIdeal S P
⊢ ↑{ val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } = ↑I * ↑J
rfl