`zeta_def`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 217/-- The arithmetic zeta function ζ (constant 1 on positive integers). -/
 218abbrev zeta : ArithmeticFunction ℕ := ArithmeticFunction.zeta
 219
 220@[simp] theorem zeta_def : zeta = ArithmeticFunction.zeta := rfl
 221
 222/-- ζ(n) = 1 for n ≥ 1. -/
 223theorem zeta_apply {n : ℕ} (hn : n ≠ 0) : zeta n = 1 := by
 224  simp only [zeta, ArithmeticFunction.zeta_apply, hn, ↓reduceIte]
 225
 226/-- ζ(0) = 0. -/
 227theorem zeta_zero : zeta 0 = 0 := by
 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

papers checked against this theorem

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