R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : Ideal.IsPrime I
hd : Disjoint ↑M ↑I
⊢ Ideal.IsPrime I ∧ Disjoint ↑M ↑I
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : Ideal.IsPrime I
hd : Disjoint ↑M ↑I
⊢ Ideal.IsPrime (Ideal.map (algebraMap R S) I)
rw [isPrime_iff_isPrime_disjoint M S, comap_map_of_isPrime_disjoint M S I hp hd]
no goals
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hp : Ideal.IsPrime I
hd : Disjoint ↑M ↑I
⊢ Ideal.IsPrime I ∧ Disjoint ↑M ↑I
exact ⟨hp, hd⟩