OAI/Combinatorics/Progressions/Lattices/FiniteUnchargedPrimeDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_prime_depth_mass line 10
  2. theorem OAI.Erdos3.finiteCharacter_order_dvd_of_annihilation line 34
  3. theorem OAI.Erdos3.finiteCharacter_uncharged_prime_mass line 41
  4. theorem OAI.Erdos3.finiteImage_uncharged_prime_density line 98
  5. theorem OAI.Erdos3.finiteImage_uncharged_prime_density_rpow line 119
  6. theorem OAI.Erdos3.finiteImage_uncharged_prime_quotient_density line 140