theorem proved term proof

`vonMangoldt_sum_divisors`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 761theorem vonMangoldt_sum_divisors {n : ℕ} :
 762    ∑ d ∈ n.divisors, vonMangoldt d = Real.log n := by

proof body

Term-mode proof.

 763  simp only [vonMangoldt]
 764  exact ArithmeticFunction.vonMangoldt_sum
 765
 766/-! ### Sigma multiplicativity helpers -/
 767
 768/-- σ_k(mn) = σ_k(m) × σ_k(n) for coprime m, n. -/

depends on (2)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
vonMangoldt in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use