OAI/Analysis/MutuallyUnbiased/GramFunctions/Block4.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramFunctions.Block4.shape line 7
2. def OAI.MUB6.Certificate.GramFunctions.Block4.decimalExponent line 8
3. def OAI.MUB6.Certificate.GramFunctions.Block4.seed0 line 10
4. def OAI.MUB6.Certificate.GramFunctions.Block4.terms0 line 12
5. def OAI.MUB6.Certificate.GramFunctions.Block4.form0 line 33
6. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced0 line 35
7. def OAI.MUB6.Certificate.GramFunctions.Block4.seed1 line 40
8. def OAI.MUB6.Certificate.GramFunctions.Block4.terms1 line 42
9. def OAI.MUB6.Certificate.GramFunctions.Block4.form1 line 65
10. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced1 line 67
11. def OAI.MUB6.Certificate.GramFunctions.Block4.seed2 line 72
12. def OAI.MUB6.Certificate.GramFunctions.Block4.terms2 line 74
13. def OAI.MUB6.Certificate.GramFunctions.Block4.form2 line 97
14. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced2 line 99
15. def OAI.MUB6.Certificate.GramFunctions.Block4.seed3 line 104
16. def OAI.MUB6.Certificate.GramFunctions.Block4.terms3 line 106
17. def OAI.MUB6.Certificate.GramFunctions.Block4.form3 line 129
18. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced3 line 131
19. def OAI.MUB6.Certificate.GramFunctions.Block4.seed4 line 136
20. def OAI.MUB6.Certificate.GramFunctions.Block4.terms4 line 138
21. def OAI.MUB6.Certificate.GramFunctions.Block4.form4 line 161
22. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced4 line 163
23. def OAI.MUB6.Certificate.GramFunctions.Block4.seed5 line 168
24. def OAI.MUB6.Certificate.GramFunctions.Block4.terms5 line 170
25. def OAI.MUB6.Certificate.GramFunctions.Block4.form5 line 191
26. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced5 line 193
27. def OAI.MUB6.Certificate.GramFunctions.Block4.seed6 line 198
28. def OAI.MUB6.Certificate.GramFunctions.Block4.terms6 line 200
29. def OAI.MUB6.Certificate.GramFunctions.Block4.form6 line 239
30. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced6 line 241
31. def OAI.MUB6.Certificate.GramFunctions.Block4.seed7 line 246
32. def OAI.MUB6.Certificate.GramFunctions.Block4.terms7 line 248
33. def OAI.MUB6.Certificate.GramFunctions.Block4.form7 line 261
34. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced7 line 263
35. def OAI.MUB6.Certificate.GramFunctions.Block4.seed8 line 268
36. def OAI.MUB6.Certificate.GramFunctions.Block4.terms8 line 270
37. def OAI.MUB6.Certificate.GramFunctions.Block4.form8 line 293
38. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced8 line 295
39. def OAI.MUB6.Certificate.GramFunctions.Block4.seed9 line 300
40. def OAI.MUB6.Certificate.GramFunctions.Block4.terms9 line 302
41. def OAI.MUB6.Certificate.GramFunctions.Block4.form9 line 315
42. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced9 line 317
43. def OAI.MUB6.Certificate.GramFunctions.Block4.seed10 line 322
44. def OAI.MUB6.Certificate.GramFunctions.Block4.terms10 line 324
45. def OAI.MUB6.Certificate.GramFunctions.Block4.form10 line 363
46. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced10 line 365
47. def OAI.MUB6.Certificate.GramFunctions.Block4.seed11 line 370
48. def OAI.MUB6.Certificate.GramFunctions.Block4.terms11 line 372
49. def OAI.MUB6.Certificate.GramFunctions.Block4.form11 line 395
50. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced11 line 397
51. def OAI.MUB6.Certificate.GramFunctions.Block4.seed12 line 402
52. def OAI.MUB6.Certificate.GramFunctions.Block4.terms12 line 404
53. def OAI.MUB6.Certificate.GramFunctions.Block4.form12 line 434
54. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced12 line 436
55. def OAI.MUB6.Certificate.GramFunctions.Block4.seed13 line 441
56. def OAI.MUB6.Certificate.GramFunctions.Block4.terms13 line 443
57. def OAI.MUB6.Certificate.GramFunctions.Block4.form13 line 482
58. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced13 line 484
59. def OAI.MUB6.Certificate.GramFunctions.Block4.seed14 line 489
60. def OAI.MUB6.Certificate.GramFunctions.Block4.terms14 line 491
61. def OAI.MUB6.Certificate.GramFunctions.Block4.form14 line 530
62. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced14 line 532
63. def OAI.MUB6.Certificate.GramFunctions.Block4.seed15 line 537
64. def OAI.MUB6.Certificate.GramFunctions.Block4.terms15 line 539
65. def OAI.MUB6.Certificate.GramFunctions.Block4.form15 line 578
66. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced15 line 580
67. def OAI.MUB6.Certificate.GramFunctions.Block4.seed16 line 585
68. def OAI.MUB6.Certificate.GramFunctions.Block4.terms16 line 587
69. def OAI.MUB6.Certificate.GramFunctions.Block4.form16 line 626
70. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced16 line 628
71. def OAI.MUB6.Certificate.GramFunctions.Block4.seed17 line 633
72. def OAI.MUB6.Certificate.GramFunctions.Block4.terms17 line 635
73. def OAI.MUB6.Certificate.GramFunctions.Block4.form17 line 656
74. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced17 line 658
75. def OAI.MUB6.Certificate.GramFunctions.Block4.seed18 line 663
76. def OAI.MUB6.Certificate.GramFunctions.Block4.terms18 line 665
77. def OAI.MUB6.Certificate.GramFunctions.Block4.form18 line 688
78. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced18 line 690
79. def OAI.MUB6.Certificate.GramFunctions.Block4.seed19 line 695
80. def OAI.MUB6.Certificate.GramFunctions.Block4.terms19 line 697
81. def OAI.MUB6.Certificate.GramFunctions.Block4.form19 line 710
82. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced19 line 712
83. def OAI.MUB6.Certificate.GramFunctions.Block4.seed20 line 717
84. def OAI.MUB6.Certificate.GramFunctions.Block4.terms20 line 719
85. def OAI.MUB6.Certificate.GramFunctions.Block4.form20 line 740
86. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced20 line 742
87. def OAI.MUB6.Certificate.GramFunctions.Block4.seed21 line 747
88. def OAI.MUB6.Certificate.GramFunctions.Block4.terms21 line 749
89. def OAI.MUB6.Certificate.GramFunctions.Block4.form21 line 772
90. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced21 line 774
91. def OAI.MUB6.Certificate.GramFunctions.Block4.forms line 779
92. theorem OAI.MUB6.Certificate.GramFunctions.Block4.balanced line 782