lean_workbook_plus_68777

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Finding $\phi(462) = 120$ . So, there are 120 numbers less than $462$ that are relatively prime to $462$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68777 :
  Nat.totient 462 = 120   :=  by sorry

Source