feat(NumberTheory/ArithmeticFunction): some additional theorems for cardFactors (Ω) (leanprover-community#28941)

Author: ShreckYe

Mathlib/Data/Nat/Factors.lean

@@ -123,6 +123,9 @@ theorem primeFactorsList_eq_nil (n : ℕ) : n.primeFactorsList = [] ↔ n = 0 
     · exact primeFactorsList_zero
     · exact primeFactorsList_one
 
+theorem primeFactorsList_ne_nil (n : ℕ) : n.primeFactorsList ≠ [] ↔ 1 < n := by
+  simp [primeFactorsList_eq_nil n, one_lt_iff_ne_zero_and_ne_one]
+
 open scoped List in
 theorem eq_of_perm_primeFactorsList {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
     (h : a.primeFactorsList ~ b.primeFactorsList) : a = b := by

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -889,6 +889,14 @@ lemma cardFactors_zero : Ω 0 = 0 := by simp
 
 @[simp] theorem cardFactors_one : Ω 1 = 0 := by simp [cardFactors_apply]
 
+@[simp]
+theorem cardFactors_eq_zero_iff_eq_zero_or_one {n : ℕ} : Ω n = 0 ↔ n = 0 ∨ n = 1 := by
+  rw [cardFactors_apply, List.length_eq_zero_iff, primeFactorsList_eq_nil]
+
+@[simp]
+theorem cardFactors_pos_iff_one_lt {n : ℕ} : 0 < Ω n ↔ 1 < n := by
+  rw [cardFactors_apply, List.length_pos_iff, primeFactorsList_ne_nil]
+
 @[simp]
 theorem cardFactors_eq_one_iff_prime {n : ℕ} : Ω n = 1 ↔ n.Prime := by
   refine ⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩
@@ -927,6 +935,10 @@ lemma cardFactors_pow {m k : ℕ} : Ω (m ^ k) = k * Ω m := by
 theorem cardFactors_apply_prime_pow {p k : ℕ} (hp : p.Prime) : Ω (p ^ k) = k := by
   simp [cardFactors_pow, hp]
 
+theorem cardFactors_eq_sum_factorization {n : ℕ} :
+    Ω n = n.factorization.sum fun _ k => k := by
+  simp [cardFactors_apply, ← List.sum_toFinset_count_eq_length, Finsupp.sum]
+
 /-- `ω n` is the number of distinct prime factors of `n`. -/
 def cardDistinctFactors : ArithmeticFunction ℕ :=
   ⟨fun n => n.primeFactorsList.dedup.length, by simp⟩