R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]
no goals
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r
simp only [hr, not_true, false_or_iff, and_false_iff]