OAI/NumberTheory/Jacobsthal/Paths/FullBoxPrefixLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.ActualReferencePrefixes.reference_prefix_mem line 15
2. theorem OAI.Erdos970.NumberTheoryLean.ActualReferencePrefixes.reference_prefix_gap_floor line 27
3. theorem OAI.Erdos970.NumberTheoryLean.SelectionWordSplit.selected_word_split line 41
4. theorem OAI.Erdos970.NumberTheoryLean.BinCutPrefixGeometry.above_word_is_prefix line 96
5. theorem OAI.Erdos970.NumberTheoryLean.BinCutPrefixGeometry.above_word_product line 109
6. theorem OAI.Erdos970.NumberTheoryLean.FullBoxPrefixLower.full_box_child_gap_floor line 126