OAI/Computability/QuantumFactoring/SortedWords.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.LEWord line 18
2. instance OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.(instance at line 19) line 19
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.le_total line 22
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.le_trans line 25
5. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insert line 29
6. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort line 33
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insert_perm line 37
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insert_length line 45
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort_perm line 47
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort_length line 51
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.insert_sorted line 53
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort_sorted line 73