OAI/NumberTheory/Jacobsthal/Sieve/LastPrimeModulusCount.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_product_eq_finset line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_primeFactors line 22
  3. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_product_squarefree line 30
  4. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_mass_eq_modulusCount line 40
  5. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_survivors_eq_product_node line 48
  6. theorem OAI.Erdos970.NumberTheoryLean.StoppedModulusCount.trace_bad_edge_iff line 56
  7. theorem OAI.Erdos970.NumberTheoryLean.LastPrimeModulusCount.survivor_required_union line 85
  8. theorem OAI.Erdos970.NumberTheoryLean.LastPrimeModulusCount.below_all_last line 91
  9. theorem OAI.Erdos970.NumberTheoryLean.LastPrimeModulusCount.small_suffix_strict_cutoff line 107
  10. theorem OAI.Erdos970.NumberTheoryLean.LastPrimeModulusCount.after_survivors_eq_last_modulusCount line 139
  11. theorem OAI.Erdos970.NumberTheoryLean.LastPrimeModulusCount.frozen_survivors_eq_modulusCount line 159