OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part2.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node64 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node64_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node64_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node65 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node65_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node65_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node66 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node66_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node66_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node67 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node67_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node67_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node68 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node68_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node68_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node69 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node69_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node69_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node70 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node70_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node70_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node71 line 81
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node71_check line 83
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node71_eval line 86
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node72 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node72_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node72_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node73 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node73_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node73_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node74 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node74_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node74_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node75 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node75_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node75_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node76 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node76_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node76_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node77 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node77_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node77_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node78 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node78_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node78_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node79 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node79_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node79_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node80 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node80_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node80_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node81 line 184
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node81_check line 186
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node81_eval line 189
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node82 line 194
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node82_check line 196
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node82_eval line 199
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node83 line 204
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node83_check line 206
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node83_eval line 209
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node84 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node84_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node84_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node85 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node85_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node85_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node86 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node86_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node86_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node87 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node87_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node87_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node88 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node88_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node88_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node89 line 265
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node89_check line 267
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node89_eval line 270
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node90 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node90_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node90_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node91 line 286
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node91_check line 288
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node91_eval line 291
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node92 line 297
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node92_check line 299
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node92_eval line 302
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node93 line 307
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node93_check line 309
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node93_eval line 312
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node94 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node94_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node94_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node95 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node95_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node95_eval line 332