OAI/NumberTheory/Jacobsthal/Paths/CanonicalKeyWitness.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos970.NumberTheoryLean.CanonicalStopKey.Key line 15
2. def OAI.Erdos970.NumberTheoryLean.CanonicalStopKey.stopKey line 21
3. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopKey.stopKey_of_tagged_word line 26
4. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopKey.stopKey_witness line 33
5. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopKey.stopKey_replacement line 52
6. def OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.family line 79
7. def OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.key line 85
8. def OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.keyGroup line 90
9. theorem OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.key_some_of_mem line 94
10. theorem OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.key_mem_group line 104
11. theorem OAI.Erdos970.NumberTheoryLean.ActualStopGroupFiber.group_eq_fiber line 116
12. def OAI.Erdos970.NumberTheoryLean.CanonicalStopPartition.keys line 153
13. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopPartition.mem_keys line 159
14. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopPartition.groups_disjoint line 167
15. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopPartition.groups_union line 181
16. theorem OAI.Erdos970.NumberTheoryLean.CanonicalStopPartition.sum_over_groups line 197
17. structure OAI.Erdos970.NumberTheoryLean.CanonicalKeyWitness.Witness line 219
18. theorem OAI.Erdos970.NumberTheoryLean.CanonicalKeyWitness.key_witness_exists line 244