zeta_mul_moebius

formal source

 241  exact ArithmeticFunction.moebius_mul_coe_zeta
 242
 243/-- Symmetric form: ζ * μ = ε. -/
 244theorem zeta_mul_moebius : (↑zeta : ArithmeticFunction ℤ) * mobius = 1 := by
 245  simp only [mobius, zeta]
 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