dirichletOne

formal source

 246  exact ArithmeticFunction.coe_zeta_mul_moebius
 247
 248/-- For the identity (Dirichlet unit), we wrap ε = δ_1. -/
 249abbrev dirichletOne : ArithmeticFunction ℤ := 1
 250
 251@[simp] theorem dirichletOne_def : dirichletOne = 1 := rfl
 252
 253/-- ε(1) = 1. -/
 254theorem dirichletOne_one : dirichletOne 1 = 1 := by
 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