`zeta_isMultiplicative`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 231 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 231.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 228  simp only [zeta, ArithmeticFunction.zeta_apply, ↓reduceIte]
 229
 230/-- ζ is multiplicative. -/
 231theorem zeta_isMultiplicative : ArithmeticFunction.IsMultiplicative zeta := by
 232  simp only [zeta]
 233  exact ArithmeticFunction.isMultiplicative_zeta
 234
 235/-! ### Möbius inversion fundamentals -/
 236
 237/-- The key identity: μ * ζ = ε (the Dirichlet identity).
 238This is the foundation of Möbius inversion. -/
 239theorem moebius_mul_zeta : (mobius : ArithmeticFunction ℤ) * ↑zeta = 1 := by
 240  simp only [mobius, zeta]
 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 -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.