lean_workbook_plus_45249
OpenDefinition of Euler's totient function
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_45249 : ∀ n : ℕ, 1 < n → ∑ k in Finset.filter (fun k => Nat.gcd k n = 1) (Finset.Icc 1 n), 1 = Nat.totient n := by sorry
Source