The sum of totients over the divisors of an integer
ProvedWorkbookSyntax.plus_42311lean-workbookrepaired-notationsource-checked
For every natural number n, the sum of φ(d) over the positive divisors d of n equals n.
Notation repair: Replace the obsolete finite-sum binder in with ∈, and restore Nat and its totient notation scope. The complete proposition, divisors, summand, and quantifier are preserved.
Source: Lean-Workbook record lean_workbook_plus_42311 (Apache-2.0). Original declaration.
Preamble
import Mathlib open Nat open scoped Nat
Formal statement
theorem WorkbookSyntax.plus_42311 (n : ℕ) : ∑ k ∈ divisors n, φ k = n := by sorry
Source