R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬IsPrime (prod I J)
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ IsPrime (prod I J) → I = ⊤ ∨ J = ⊤
contrapose!
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ ¬1 ∈ I ∧ ¬1 ∈ J → ¬1 ∈ prod I J → ∃ x x_1 h, ¬x ∈ prod I J ∧ ¬x_1 ∈ prod I J
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ I ≠ ⊤ ∧ J ≠ ⊤ → ¬IsPrime (prod I J)
simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
⊢ ¬1 ∈ I ∧ ¬1 ∈ J → ¬1 ∈ prod I J → ∃ x x_1 h, ¬x ∈ prod I J ∧ ¬x_1 ∈ prod I J
exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ (0, 1) * (1, 0) ∈ prod I J
simp
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(0, 1) ∈ prod I J
simp [hJ]
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I' : Ideal R
J✝ J' : Ideal S
I : Ideal R
J : Ideal S
x✝¹ : ¬1 ∈ I ∧ ¬1 ∈ J
x✝ : ¬1 ∈ prod I J
hI : ¬1 ∈ I
hJ : ¬1 ∈ J
⊢ ¬(1, 0) ∈ prod I J
simp [hI]