OAI/NumberTheory/Jacobsthal/Paths/ReferenceHistoryAdmission.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.cap_lower_ratio line 20
2. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.uncapped_child_iff line 34
3. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.uncapped_child_invariants line 76
4. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.decreasing_cons_iff line 84
5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.referencePrefixes_cons_iff line 96
6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.reference_history_iff line 102
7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceHistoryAdmission.reference_family_eq_uncapped line 127