liouville_zero

formal source

 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]
 307  norm_num
 308
 309/-- λ(p^k) = (-1)^k for prime p. -/
 310theorem liouville_prime_pow {p k : ℕ} (hp : Prime p) :
 311    liouville (p ^ k) = (-1) ^ k := by
 312  have hp' : Nat.Prime p := (prime_iff p).1 hp
 313  cases k with
 314  | zero => simp [liouville_one]
 315  | succ k =>
 316    have hpk : p ^ (k + 1) ≠ 0 := pow_ne_zero (k + 1) hp'.ne_zero
 317    simp only [liouville, hpk, ↓reduceIte, bigOmega]
 318    -- Ω(p^k) = k for prime p