dirichletOne_ne_one

formal source

 255  simp [dirichletOne]
 256
 257/-- ε(n) = 0 for n > 1. -/
 258theorem dirichletOne_ne_one {n : ℕ} (hn : n ≠ 1) : dirichletOne n = 0 := by
 259  simp [dirichletOne, hn]
 260
 261/-! ### Additional multiplicativity lemmas -/
 262
 263/-- ω (number of distinct prime factors) is additive on coprimes: ω(mn) = ω(m) + ω(n). -/
 264theorem omega_mul_of_coprime {m n : ℕ} (_hm : m ≠ 0) (_hn : n ≠ 0) (h : Nat.Coprime m n) :
 265    omega (m * n) = omega m + omega n := by
 266  simp only [omega]
 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