no goals
α : Type u_1
β : Type ?u.327284
γ : Type ?u.327287
δ : Type ?u.327290
inst✝ : CommMonoidWithZero α
⊢ (∀ (a : α), Irreducible a ↔ Prime a) ↔ ∀ (a : Associates α), Irreducible a ↔ Prime a
simp_rw [forall_associated, irreducible_mk, prime_mk]