OAI/NumberTheory/TotientAsymptotic/TerminalPrefixMassCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retain an arbitrary restriction on the prime prefix while counting a terminal strip through its distinct residual totients.

  1. theorem OAI.TotientAsymptotic.terminal_prefix_mass_count line 12