OAI/NumberTheory/TotientAsymptotic/SmallTerminalCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Gaussian counting at the first coordinate below the fixed terminal cutoff.

  1. theorem OAI.TotientAsymptotic.small_terminal_row_count line 16