OAI/NumberTheory/Jacobsthal/Partitions/EligibleBoxLists.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.EligibleBoxLists.eligibleLists line 14
2. theorem OAI.Erdos970.NumberTheoryLean.EligibleBoxLists.mem_eligibleLists line 18
3. theorem OAI.Erdos970.NumberTheoryLean.EligibleBoxLists.eligibleLists_card line 23
4. theorem OAI.Erdos970.NumberTheoryLean.EligibleBoxLists.eligibleLists_eligible line 31
5. theorem OAI.Erdos970.NumberTheoryLean.EligibleBoxLists.soft_witness_in_eligibleLists line 37