OAI/Analysis/MutuallyUnbiased/GramFunctions/Block3.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramFunctions.Block3.shape line 7
2. def OAI.MUB6.Certificate.GramFunctions.Block3.decimalExponent line 8
3. def OAI.MUB6.Certificate.GramFunctions.Block3.seed0 line 10
4. def OAI.MUB6.Certificate.GramFunctions.Block3.terms0 line 12
5. def OAI.MUB6.Certificate.GramFunctions.Block3.form0 line 39
6. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced0 line 41
7. def OAI.MUB6.Certificate.GramFunctions.Block3.seed1 line 46
8. def OAI.MUB6.Certificate.GramFunctions.Block3.terms1 line 48
9. def OAI.MUB6.Certificate.GramFunctions.Block3.form1 line 56
10. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced1 line 58
11. def OAI.MUB6.Certificate.GramFunctions.Block3.seed2 line 63
12. def OAI.MUB6.Certificate.GramFunctions.Block3.terms2 line 65
13. def OAI.MUB6.Certificate.GramFunctions.Block3.form2 line 84
14. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced2 line 86
15. def OAI.MUB6.Certificate.GramFunctions.Block3.seed3 line 91
16. def OAI.MUB6.Certificate.GramFunctions.Block3.terms3 line 93
17. def OAI.MUB6.Certificate.GramFunctions.Block3.form3 line 112
18. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced3 line 114
19. def OAI.MUB6.Certificate.GramFunctions.Block3.seed4 line 119
20. def OAI.MUB6.Certificate.GramFunctions.Block3.terms4 line 121
21. def OAI.MUB6.Certificate.GramFunctions.Block3.form4 line 140
22. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced4 line 142
23. def OAI.MUB6.Certificate.GramFunctions.Block3.seed5 line 147
24. def OAI.MUB6.Certificate.GramFunctions.Block3.terms5 line 149
25. def OAI.MUB6.Certificate.GramFunctions.Block3.form5 line 188
26. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced5 line 190
27. def OAI.MUB6.Certificate.GramFunctions.Block3.seed6 line 195
28. def OAI.MUB6.Certificate.GramFunctions.Block3.terms6 line 197
29. def OAI.MUB6.Certificate.GramFunctions.Block3.form6 line 205
30. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced6 line 207
31. def OAI.MUB6.Certificate.GramFunctions.Block3.seed7 line 212
32. def OAI.MUB6.Certificate.GramFunctions.Block3.terms7 line 214
33. def OAI.MUB6.Certificate.GramFunctions.Block3.form7 line 241
34. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced7 line 243
35. def OAI.MUB6.Certificate.GramFunctions.Block3.seed8 line 248
36. def OAI.MUB6.Certificate.GramFunctions.Block3.terms8 line 250
37. def OAI.MUB6.Certificate.GramFunctions.Block3.form8 line 289
38. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced8 line 291
39. def OAI.MUB6.Certificate.GramFunctions.Block3.seed9 line 296
40. def OAI.MUB6.Certificate.GramFunctions.Block3.terms9 line 298
41. def OAI.MUB6.Certificate.GramFunctions.Block3.form9 line 337
42. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced9 line 339
43. def OAI.MUB6.Certificate.GramFunctions.Block3.seed10 line 344
44. def OAI.MUB6.Certificate.GramFunctions.Block3.terms10 line 346
45. def OAI.MUB6.Certificate.GramFunctions.Block3.form10 line 365
46. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced10 line 367
47. def OAI.MUB6.Certificate.GramFunctions.Block3.seed11 line 372
48. def OAI.MUB6.Certificate.GramFunctions.Block3.terms11 line 374
49. def OAI.MUB6.Certificate.GramFunctions.Block3.form11 line 385
50. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced11 line 387
51. def OAI.MUB6.Certificate.GramFunctions.Block3.seed12 line 392
52. def OAI.MUB6.Certificate.GramFunctions.Block3.terms12 line 394
53. def OAI.MUB6.Certificate.GramFunctions.Block3.form12 line 405
54. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced12 line 407
55. def OAI.MUB6.Certificate.GramFunctions.Block3.seed13 line 412
56. def OAI.MUB6.Certificate.GramFunctions.Block3.terms13 line 414
57. def OAI.MUB6.Certificate.GramFunctions.Block3.form13 line 433
58. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced13 line 435
59. def OAI.MUB6.Certificate.GramFunctions.Block3.seed14 line 440
60. def OAI.MUB6.Certificate.GramFunctions.Block3.terms14 line 442
61. def OAI.MUB6.Certificate.GramFunctions.Block3.form14 line 453
62. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced14 line 455
63. def OAI.MUB6.Certificate.GramFunctions.Block3.seed15 line 460
64. def OAI.MUB6.Certificate.GramFunctions.Block3.terms15 line 462
65. def OAI.MUB6.Certificate.GramFunctions.Block3.form15 line 481
66. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced15 line 483
67. def OAI.MUB6.Certificate.GramFunctions.Block3.seed16 line 488
68. def OAI.MUB6.Certificate.GramFunctions.Block3.terms16 line 490
69. def OAI.MUB6.Certificate.GramFunctions.Block3.form16 line 501
70. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced16 line 503
71. def OAI.MUB6.Certificate.GramFunctions.Block3.seed17 line 508
72. def OAI.MUB6.Certificate.GramFunctions.Block3.terms17 line 510
73. def OAI.MUB6.Certificate.GramFunctions.Block3.form17 line 537
74. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced17 line 539
75. def OAI.MUB6.Certificate.GramFunctions.Block3.seed18 line 544
76. def OAI.MUB6.Certificate.GramFunctions.Block3.terms18 line 546
77. def OAI.MUB6.Certificate.GramFunctions.Block3.form18 line 573
78. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced18 line 575
79. def OAI.MUB6.Certificate.GramFunctions.Block3.seed19 line 580
80. def OAI.MUB6.Certificate.GramFunctions.Block3.terms19 line 582
81. def OAI.MUB6.Certificate.GramFunctions.Block3.form19 line 595
82. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced19 line 597
83. def OAI.MUB6.Certificate.GramFunctions.Block3.seed20 line 602
84. def OAI.MUB6.Certificate.GramFunctions.Block3.terms20 line 604
85. def OAI.MUB6.Certificate.GramFunctions.Block3.form20 line 612
86. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced20 line 614
87. def OAI.MUB6.Certificate.GramFunctions.Block3.seed21 line 619
88. def OAI.MUB6.Certificate.GramFunctions.Block3.terms21 line 621
89. def OAI.MUB6.Certificate.GramFunctions.Block3.form21 line 660
90. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced21 line 662
91. def OAI.MUB6.Certificate.GramFunctions.Block3.seed22 line 667
92. def OAI.MUB6.Certificate.GramFunctions.Block3.terms22 line 669
93. def OAI.MUB6.Certificate.GramFunctions.Block3.form22 line 708
94. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced22 line 710
95. def OAI.MUB6.Certificate.GramFunctions.Block3.seed23 line 715
96. def OAI.MUB6.Certificate.GramFunctions.Block3.terms23 line 717
97. def OAI.MUB6.Certificate.GramFunctions.Block3.form23 line 738
98. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced23 line 740
99. def OAI.MUB6.Certificate.GramFunctions.Block3.seed24 line 745
100. def OAI.MUB6.Certificate.GramFunctions.Block3.terms24 line 747
101. def OAI.MUB6.Certificate.GramFunctions.Block3.form24 line 755
102. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced24 line 757
103. def OAI.MUB6.Certificate.GramFunctions.Block3.seed25 line 762
104. def OAI.MUB6.Certificate.GramFunctions.Block3.terms25 line 764
105. def OAI.MUB6.Certificate.GramFunctions.Block3.form25 line 775
106. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced25 line 777
107. def OAI.MUB6.Certificate.GramFunctions.Block3.seed26 line 782
108. def OAI.MUB6.Certificate.GramFunctions.Block3.terms26 line 784
109. def OAI.MUB6.Certificate.GramFunctions.Block3.form26 line 811
110. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced26 line 813
111. def OAI.MUB6.Certificate.GramFunctions.Block3.forms line 818
112. theorem OAI.MUB6.Certificate.GramFunctions.Block3.balanced line 821