OAI/NumberTheory/PowerFree/PrimePools.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.physicalPathProduct line 18
  2. theorem OAI.QuarticPowerFree.physical_minor_dvd_pathProduct line 24
  3. def OAI.QuarticPowerFree.PhysicalRegular line 34
  4. theorem OAI.QuarticPowerFree.filter_card_le_of_fraction line 40
  5. theorem OAI.QuarticPowerFree.PhysicalRegular.bad_minor line 52
  6. theorem OAI.QuarticPowerFree.cumulative_good_prime_product line 70
  7. def OAI.QuarticPowerFree.firstStop line 122
  8. theorem OAI.QuarticPowerFree.firstStop_le line 125
  9. theorem OAI.QuarticPowerFree.firstStop_spec line 128
  10. theorem OAI.QuarticPowerFree.firstStop_not_before line 131
  11. theorem OAI.QuarticPowerFree.dimension_until_firstStop line 134
  12. theorem OAI.QuarticPowerFree.firstStop_terminal line 153
  13. theorem OAI.QuarticPowerFree.physical_fiber_le_points line 168
  14. theorem OAI.QuarticPowerFree.physical_dimension_mono line 195
  15. theorem OAI.QuarticPowerFree.physical_stopped_count line 213
  16. theorem OAI.QuarticPowerFree.finite_prime_pool line 273
  17. theorem OAI.QuarticPowerFree.disjoint_prime_pools line 292