OAI/NumberTheory/TotientAsymptotic/UnbandedSimplexMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The prime-prefix mass bound used before the first failed simplex row.

  1. theorem OAI.TotientAsymptotic.unbanded_simplex_prime_mass line 14