R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (prod ⊤ I)
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
⊢ IsPrime (prod ⊤ I)
letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod I ⊤))
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (prod ⊤ I)
rw [← map_prodComm_prod]
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J J' I : Ideal S
h : IsPrime I
this : IsPrime (prod I ⊤) := isPrime_ideal_prod_top
⊢ IsPrime (map (↑RingEquiv.prodComm) (prod I ⊤))
apply map_isPrime_of_equiv _