lean_workbook_plus_71300
ProvedThus we want the number of such that is reduced and satisfies It is easy to see that this holds exactly for , and so we want the number of coprime to in this range. , but we don't want to count and , so we get occurrences of the number .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71300 : Finset.card (Finset.filter (λ k => Nat.gcd 2013 k = 1) (Finset.Icc 3 2012)) = 1198 := by sorry
Source