bigOmega_pow

formal source

 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
 301  have hp' : Nat.Prime p := (prime_iff p).1 hp
 302  have hp_ne : p ≠ 0 := hp'.ne_zero
 303  simp only [liouville, hp_ne, ↓reduceIte, bigOmega]
 304  -- Ω(p) = 1 for prime p
 305  have hOmega : ArithmeticFunction.cardFactors p = 1 := ArithmeticFunction.cardFactors_apply_prime hp'
 306  rw [hOmega]