case intro.intro
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)
α : Type u_1
inst✝ : CommRing α
p : α
hp : Prime p
⊢ Prime (-p)
obtain ⟨h1, h2, h3⟩ := hp
no goals
case intro.intro
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)
exact ⟨neg_ne_zero.mpr h1, by rwa [IsUnit.neg_iff], by simpa [neg_dvd] using h3⟩
no goals
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ¬IsUnit (-p)
rwa [IsUnit.neg_iff]
no goals
α : Type u_1
inst✝ : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ∀ (a b : α), -p ∣ a * b → -p ∣ a ∨ -p ∣ b
simpa [neg_dvd] using h3