[STATEMENT]
lemma primes_omega_eq_0_iff: "primes_omega n = 0 \<longleftrightarrow> n = 0 \<or> n = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (primes_omega n = 0) = (n = 0 \<or> n = 1)
[PROOF STEP]
by (auto simp: primes_omega_def prime_factorization_empty_iff)