OAI/Combinatorics/SquareDifference/PrimeSetup.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SquareDifference.SourcePrimeHyp line 11
  2. lemma OAI.SquareDifference.SourcePrimeHyp.mono line 21
  3. def OAI.SquareDifference.smallPrimeSet line 26
  4. def OAI.SquareDifference.largePrimeSet line 28
  5. abbrev OAI.SquareDifference.SmallPrime line 30
  6. abbrev OAI.SquareDifference.LargePrime line 32
  7. def OAI.SquareDifference.smallPrimes line 34
  8. def OAI.SquareDifference.largePrimes line 36
  9. instance OAI.SquareDifference.smallPrimes_fact line 38
  10. instance OAI.SquareDifference.largePrimes_fact line 41
  11. lemma OAI.SquareDifference.smallPrimes_lt line 44
  12. lemma OAI.SquareDifference.largePrimes_ge line 46
  13. lemma OAI.SquareDifference.smallPrimes_injective line 48
  14. lemma OAI.SquareDifference.actualPrime_injective line 50
  15. lemma OAI.SquareDifference.actualPrime_cover line 60
  16. lemma OAI.SquareDifference.smallQuadraticModulus_coprime line 66
  17. lemma OAI.SquareDifference.actualPrime_coprime line 74
  18. lemma OAI.SquareDifference.actualSmallModulus_ge_two line 83
  19. lemma OAI.SquareDifference.actualPrime_hyp line 91