OAI/NumberTheory/Jacobsthal/Partitions/RegularityDefectPartition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.ActualRegularBoxes.regularWords line 17
2. def OAI.Erdos970.NumberTheoryLean.ActualRegularBoxes.regularBoxes line 24
3. theorem OAI.Erdos970.NumberTheoryLean.ActualRegularBoxes.regular_word_anchor line 29
4. theorem OAI.Erdos970.NumberTheoryLean.ActualRegularBoxes.regular_boxes_anchors line 41
5. theorem OAI.Erdos970.NumberTheoryLean.ActualRegularBoxes.regular_boxes_search_singletons line 49
6. def OAI.Erdos970.NumberTheoryLean.RegularityDefectPartition.lengthFailure line 71
7. def OAI.Erdos970.NumberTheoryLean.RegularityDefectPartition.clearanceFailure line 72
8. theorem OAI.Erdos970.NumberTheoryLean.RegularityDefectPartition.regularity_defect_sum line 74