OAI/NumberTheory/TotientAsymptotic/LocalOriginalPruning.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two direct exceptions and the surviving comparison case cover the actual original-head bad candidates.

  1. theorem OAI.TotientAsymptotic.local_original_count_of_regular line 12