Lean-Workbook Syntax 45249: Counting integers coprime to n

Proved

WorkbookSyntax.plus_45249

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For every natural $n>1$ , the number of integers $k$ with $1\le k\le n$ and $\gcd(k,n)=1$ equals $\varphi(n)$ .

Source: Lean-Workbook row lean_workbook_plus_45249 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Data.Nat.Totient

Formal statement

theorem WorkbookSyntax.plus_45249 : ∀ n : ℕ, 1 < n → ∑ k ∈ Finset.filter (fun k => Nat.gcd k n = 1) (Finset.Icc 1 n), 1 = Nat.totient n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_45249; immutable original Prove2Me node 1e10d4c4-addf-4a3d-b30e-5ee36a2843d3

View graph