OAI/NumberTheory/TotientAsymptotic/FordNormalCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normal-value upper count, with the exponent in Ford's coefficient form.

  1. theorem OAI.TotientAsymptotic.ford_normal_value_count line 11