bigOmega_mul

formal source

 267  exact ArithmeticFunction.cardDistinctFactors_mul h
 268
 269/-- Ω (number of prime factors with multiplicity) is additive: Ω(mn) = Ω(m) + Ω(n). -/
 270theorem bigOmega_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
 271    bigOmega (m * n) = bigOmega m + bigOmega n := by
 272  simp only [bigOmega]
 273  exact ArithmeticFunction.cardFactors_mul hm hn
 274
 275/-- Ω is completely additive on powers: Ω(n^k) = k * Ω(n). -/
 276theorem bigOmega_pow {n k : ℕ} : bigOmega (n ^ k) = k * bigOmega n := by
 277  simp only [bigOmega]
 278  exact ArithmeticFunction.cardFactors_pow
 279
 280/-! ### Liouville function λ -/
 281
 282/-- The Liouville function λ(n) = (-1)^Ω(n).
 283Note: We define this directly since Mathlib may not have a prebuilt version. -/
 284def liouville (n : ℕ) : ℤ :=
 285  if n = 0 then 0 else (-1) ^ bigOmega n
 286
 287/-- λ(0) = 0 (by convention). -/
 288@[simp] theorem liouville_zero : liouville 0 = 0 := by
 289  simp [liouville]
 290
 291/-- λ(n) = (-1)^Ω(n) for n ≠ 0. -/
 292theorem liouville_eq {n : ℕ} (hn : n ≠ 0) : liouville n = (-1) ^ bigOmega n := by
 293  simp [liouville, hn]
 294
 295/-- λ(1) = 1. -/
 296theorem liouville_one : liouville 1 = 1 := by
 297  simp [liouville, bigOmega_apply]
 298
 299/-- λ(p) = -1 for prime p. -/
 300theorem liouville_prime {p : ℕ} (hp : Prime p) : liouville p = -1 := by