OAI/NumberTheory/Jacobsthal/Partitions/ParentEdgeCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosInverseHits.sourceParentBase line 14
  2. theorem OAI.Erdos970.ErdosInverseHits.sourceParentBase_bounds line 18
  3. theorem OAI.Erdos970.ErdosInverseHits.source_parent_hits_iff line 24
  4. def OAI.Erdos970.ErdosInverseHits.parentSurvivorCoordinates line 33
  5. theorem OAI.Erdos970.ErdosInverseHits.modulusCandidates_eq_parent_image line 39
  6. theorem OAI.Erdos970.ErdosInverseHits.modulusCount_eq_parent_card line 61
  7. theorem OAI.Erdos970.ErdosInverseHits.source_parent_length_error line 72
  8. def OAI.Erdos970.ErdosInverseHits.parentEdgeResidue line 88
  9. theorem OAI.Erdos970.ErdosInverseHits.parent_edge_hit_iff line 93
  10. theorem OAI.Erdos970.ErdosInverseHits.modulusCandidates_eq_edge_image line 104
  11. theorem OAI.Erdos970.ErdosInverseHits.modulusCount_eq_edge_card line 122