OAI/Analysis/MutuallyUnbiased/GramFunctions/Block1.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramFunctions.Block1.shape line 7
2. def OAI.MUB6.Certificate.GramFunctions.Block1.decimalExponent line 8
3. def OAI.MUB6.Certificate.GramFunctions.Block1.seed0 line 10
4. def OAI.MUB6.Certificate.GramFunctions.Block1.terms0 line 12
5. def OAI.MUB6.Certificate.GramFunctions.Block1.form0 line 45
6. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced0 line 47
7. def OAI.MUB6.Certificate.GramFunctions.Block1.seed1 line 52
8. def OAI.MUB6.Certificate.GramFunctions.Block1.terms1 line 54
9. def OAI.MUB6.Certificate.GramFunctions.Block1.form1 line 71
10. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced1 line 73
11. def OAI.MUB6.Certificate.GramFunctions.Block1.seed2 line 78
12. def OAI.MUB6.Certificate.GramFunctions.Block1.terms2 line 80
13. def OAI.MUB6.Certificate.GramFunctions.Block1.form2 line 113
14. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced2 line 115
15. def OAI.MUB6.Certificate.GramFunctions.Block1.seed3 line 120
16. def OAI.MUB6.Certificate.GramFunctions.Block1.terms3 line 122
17. def OAI.MUB6.Certificate.GramFunctions.Block1.form3 line 139
18. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced3 line 141
19. def OAI.MUB6.Certificate.GramFunctions.Block1.seed4 line 146
20. def OAI.MUB6.Certificate.GramFunctions.Block1.terms4 line 148
21. def OAI.MUB6.Certificate.GramFunctions.Block1.form4 line 165
22. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced4 line 167
23. def OAI.MUB6.Certificate.GramFunctions.Block1.seed5 line 172
24. def OAI.MUB6.Certificate.GramFunctions.Block1.terms5 line 174
25. def OAI.MUB6.Certificate.GramFunctions.Block1.form5 line 207
26. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced5 line 209
27. def OAI.MUB6.Certificate.GramFunctions.Block1.seed6 line 214
28. def OAI.MUB6.Certificate.GramFunctions.Block1.terms6 line 216
29. def OAI.MUB6.Certificate.GramFunctions.Block1.form6 line 233
30. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced6 line 235
31. def OAI.MUB6.Certificate.GramFunctions.Block1.seed7 line 240
32. def OAI.MUB6.Certificate.GramFunctions.Block1.terms7 line 242
33. def OAI.MUB6.Certificate.GramFunctions.Block1.form7 line 275
34. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced7 line 277
35. def OAI.MUB6.Certificate.GramFunctions.Block1.seed8 line 282
36. def OAI.MUB6.Certificate.GramFunctions.Block1.terms8 line 284
37. def OAI.MUB6.Certificate.GramFunctions.Block1.form8 line 301
38. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced8 line 303
39. def OAI.MUB6.Certificate.GramFunctions.Block1.seed9 line 308
40. def OAI.MUB6.Certificate.GramFunctions.Block1.terms9 line 310
41. def OAI.MUB6.Certificate.GramFunctions.Block1.form9 line 343
42. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced9 line 345
43. def OAI.MUB6.Certificate.GramFunctions.Block1.seed10 line 350
44. def OAI.MUB6.Certificate.GramFunctions.Block1.terms10 line 352
45. def OAI.MUB6.Certificate.GramFunctions.Block1.form10 line 369
46. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced10 line 371
47. def OAI.MUB6.Certificate.GramFunctions.Block1.seed11 line 376
48. def OAI.MUB6.Certificate.GramFunctions.Block1.terms11 line 378
49. def OAI.MUB6.Certificate.GramFunctions.Block1.form11 line 395
50. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced11 line 397
51. def OAI.MUB6.Certificate.GramFunctions.Block1.seed12 line 402
52. def OAI.MUB6.Certificate.GramFunctions.Block1.terms12 line 404
53. def OAI.MUB6.Certificate.GramFunctions.Block1.form12 line 437
54. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced12 line 439
55. def OAI.MUB6.Certificate.GramFunctions.Block1.seed13 line 444
56. def OAI.MUB6.Certificate.GramFunctions.Block1.terms13 line 446
57. def OAI.MUB6.Certificate.GramFunctions.Block1.form13 line 463
58. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced13 line 465
59. def OAI.MUB6.Certificate.GramFunctions.Block1.seed14 line 470
60. def OAI.MUB6.Certificate.GramFunctions.Block1.terms14 line 472
61. def OAI.MUB6.Certificate.GramFunctions.Block1.form14 line 499
62. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced14 line 501
63. def OAI.MUB6.Certificate.GramFunctions.Block1.seed15 line 506
64. def OAI.MUB6.Certificate.GramFunctions.Block1.terms15 line 508
65. def OAI.MUB6.Certificate.GramFunctions.Block1.form15 line 541
66. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced15 line 543
67. def OAI.MUB6.Certificate.GramFunctions.Block1.seed16 line 548
68. def OAI.MUB6.Certificate.GramFunctions.Block1.terms16 line 550
69. def OAI.MUB6.Certificate.GramFunctions.Block1.form16 line 571
70. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced16 line 573
71. def OAI.MUB6.Certificate.GramFunctions.Block1.seed17 line 578
72. def OAI.MUB6.Certificate.GramFunctions.Block1.terms17 line 580
73. def OAI.MUB6.Certificate.GramFunctions.Block1.form17 line 613
74. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced17 line 615
75. def OAI.MUB6.Certificate.GramFunctions.Block1.seed18 line 620
76. def OAI.MUB6.Certificate.GramFunctions.Block1.terms18 line 622
77. def OAI.MUB6.Certificate.GramFunctions.Block1.form18 line 655
78. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced18 line 657
79. def OAI.MUB6.Certificate.GramFunctions.Block1.seed19 line 662
80. def OAI.MUB6.Certificate.GramFunctions.Block1.terms19 line 664
81. def OAI.MUB6.Certificate.GramFunctions.Block1.form19 line 681
82. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced19 line 683
83. def OAI.MUB6.Certificate.GramFunctions.Block1.seed20 line 688
84. def OAI.MUB6.Certificate.GramFunctions.Block1.terms20 line 690
85. def OAI.MUB6.Certificate.GramFunctions.Block1.form20 line 711
86. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced20 line 713
87. def OAI.MUB6.Certificate.GramFunctions.Block1.forms line 718
88. theorem OAI.MUB6.Certificate.GramFunctions.Block1.balanced line 721