OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row12.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_0 line 16
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_0 line 18
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_0 line 22
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_0 line 54
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_1 line 61
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_1 line 63
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_1 line 67
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_1 line 99
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_2 line 106
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_2 line 108
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_2 line 112
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_2 line 144
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_3 line 151
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_3 line 153
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_3 line 157
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_3 line 189
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_4 line 196
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_4 line 198
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_4 line 202
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_4 line 234
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_5 line 241
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_5 line 243
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_5 line 247
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_5 line 279
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_6 line 286
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_6 line 288
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_6 line 292
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_6 line 324
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_7 line 331
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_7 line 333
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_7 line 337
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_7 line 369
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_8 line 376
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_8 line 378
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_8 line 382
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_8 line 414
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_9 line 421
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_9 line 423
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_9 line 427
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_9 line 459
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_10 line 466
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_10 line 468
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_10 line 472
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_10 line 504
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_11 line 511
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_11 line 513
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_11 line 517
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_11 line 549
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows12_12 line 556
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck12_12 line 558
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound12_12 line 562
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval12_12 line 594