OAI/NumberTheory/Ostmann/Supply/FavorableTailPrimeMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Proposition 5.1: favorable primes for the actual infinite summand tails

  1. theorem OAI.Ostmann.EventuallyPrimeSumset.favorable_tail_prime_mass line 13