OAI/Combinatorics/FiniteCircle/Primes.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.primeInterval line 9
  2. theorem OAI.FiniteCircle.centralBinom_le_interval line 11
  3. theorem OAI.FiniteCircle.centralBinom_le_interval_card line 80
  4. theorem OAI.FiniteCircle.log_le_linear_million line 88
  5. theorem OAI.FiniteCircle.primeInterval_card_cubic line 101
  6. theorem OAI.FiniteCircle.prime_array line 154
  7. structure OAI.FiniteCircle.StandingPrimes line 184
  8. theorem OAI.FiniteCircle.standingPrimes_exists line 189
  9. theorem OAI.FiniteCircle.StandingPrimes.atLevel line 198
  10. theorem OAI.FiniteCircle.StandingPrimes.positive line 203
  11. theorem OAI.FiniteCircle.StandingPrimes.level_injective line 209
  12. theorem OAI.FiniteCircle.StandingPrimes.level_distinct line 216
  13. theorem OAI.FiniteCircle.StandingPrimes.coprime line 226
  14. theorem OAI.FiniteCircle.StandingPrimes.period_pos line 236
  15. theorem OAI.FiniteCircle.StandingPrimes.circle_pos line 239
  16. theorem OAI.FiniteCircle.StandingPrimes.circle_even line 244
  17. theorem OAI.FiniteCircle.StandingPrimes.divides_circle line 248
  18. theorem OAI.FiniteCircle.StandingPrimes.maskPrimes line 259
  19. theorem OAI.FiniteCircle.StandingPrimes.excludedPrimes line 262