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 : Ideal R
⊢ ↑(I * J) = { val := ↑↑I * ↑↑J, property := (_ : IsFractional S (↑↑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 : Ideal R
⊢ ↑(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 : Ideal R
⊢ ↑(I * J) = { val := ↑↑I * ↑↑J, property := (_ : IsFractional S (↑↑I * ↑↑J)) }
exact coeToSubmodule_injective (coeSubmodule_mul _ _ _)