OAI/NumberTheory/Jacobsthal/Sieve/CofactorAllChoiceBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.parentCofactorMultiplicity line 16
  2. def OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.completeParent line 18
  3. theorem OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.cofactor_slots_zero line 21
  4. theorem OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.cofactor_total_le line 25
  5. theorem OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.complete_parent_mem line 32
  6. theorem OAI.Erdos970.NumberTheoryLean.ParentCofactorChoices.complete_parent_product line 40
  7. theorem OAI.Erdos970.NumberTheoryLean.CofactorAllChoiceBounds.cofactor_all_choice_lengths line 62