OAI/Analysis/MutuallyUnbiased/GramEntries/Block5Row10.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_0 line 14
2. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_0 line 16
3. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_0 line 20
4. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_0 line 45
5. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_1 line 52
6. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_1 line 54
7. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_1 line 58
8. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_1 line 83
9. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_2 line 90
10. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_2 line 92
11. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_2 line 96
12. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_2 line 121
13. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_3 line 128
14. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_3 line 130
15. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_3 line 134
16. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_3 line 159
17. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_4 line 166
18. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_4 line 168
19. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_4 line 172
20. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_4 line 197
21. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_5 line 204
22. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_5 line 206
23. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_5 line 210
24. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_5 line 235
25. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_6 line 242
26. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_6 line 244
27. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_6 line 248
28. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_6 line 273
29. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_7 line 280
30. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_7 line 282
31. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_7 line 286
32. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_7 line 311
33. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_8 line 318
34. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_8 line 320
35. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_8 line 324
36. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_8 line 349
37. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_9 line 356
38. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_9 line 358
39. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_9 line 362
40. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_9 line 387
41. def OAI.MUB6.Certificate.GramEntries.Block5.rows10_10 line 394
42. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck10_10 line 396
43. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound10_10 line 400
44. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval10_10 line 425