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 K : FractionalIdeal S P
⊢ { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } ≤ K ↔ ∀ (i : P), i ∈ I → ∀ (j : P), j ∈ J → i * j ∈ K
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 K : FractionalIdeal S P
⊢ I * J ≤ K ↔ ∀ (i : P), i ∈ I → ∀ (j : P), j ∈ J → i * j ∈ K
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 K : FractionalIdeal S P
⊢ { val := ↑I * ↑J, property := (_ : IsFractional S (↑I * ↑J)) } ≤ K ↔ ∀ (i : P), i ∈ I → ∀ (j : P), j ∈ J → i * j ∈ K
exact Submodule.mul_le