OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part21.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node672 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node672_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node672_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node673 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node673_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node673_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node674 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node674_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node674_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node675 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node675_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node675_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node676 line 48
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node676_check line 50
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node676_eval line 53
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node677 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node677_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node677_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node678 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node678_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node678_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node679 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node679_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node679_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node680 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node680_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node680_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node681 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node681_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node681_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node682 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node682_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node682_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node683 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node683_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node683_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node684 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node684_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node684_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node685 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node685_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node685_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node686 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node686_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node686_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node687 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node687_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node687_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node688 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node688_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node688_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node689 line 181
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node689_check line 183
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node689_eval line 186
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node690 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node690_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node690_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node691 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node691_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node691_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node692 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node692_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node692_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node693 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node693_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node693_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node694 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node694_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node694_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node695 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node695_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node695_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node696 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node696_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node696_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node697 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node697_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node697_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node698 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node698_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node698_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node699 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node699_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node699_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node700 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node700_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node700_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node701 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node701_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node701_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node702 line 313
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node702_check line 315
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node702_eval line 318
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node703 line 322
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node703_check line 324
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node703_eval line 327