OAI/Analysis/MutuallyUnbiased/GramEntries/Block5Data.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block5.entry0_0 line 31
  2. def OAI.MUB6.Certificate.GramEntries.Block5.entry1_0 line 33
  3. def OAI.MUB6.Certificate.GramEntries.Block5.entry1_1 line 35
  4. def OAI.MUB6.Certificate.GramEntries.Block5.entry2_0 line 37
  5. def OAI.MUB6.Certificate.GramEntries.Block5.entry2_1 line 39
  6. def OAI.MUB6.Certificate.GramEntries.Block5.entry2_2 line 41
  7. def OAI.MUB6.Certificate.GramEntries.Block5.entry3_0 line 43
  8. def OAI.MUB6.Certificate.GramEntries.Block5.entry3_1 line 45
  9. def OAI.MUB6.Certificate.GramEntries.Block5.entry3_2 line 47
  10. def OAI.MUB6.Certificate.GramEntries.Block5.entry3_3 line 49
  11. def OAI.MUB6.Certificate.GramEntries.Block5.entry4_0 line 51
  12. def OAI.MUB6.Certificate.GramEntries.Block5.entry4_1 line 53
  13. def OAI.MUB6.Certificate.GramEntries.Block5.entry4_2 line 55
  14. def OAI.MUB6.Certificate.GramEntries.Block5.entry4_3 line 57
  15. def OAI.MUB6.Certificate.GramEntries.Block5.entry4_4 line 59
  16. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_0 line 61
  17. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_1 line 63
  18. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_2 line 65
  19. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_3 line 67
  20. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_4 line 69
  21. def OAI.MUB6.Certificate.GramEntries.Block5.entry5_5 line 71
  22. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_0 line 73
  23. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_1 line 75
  24. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_2 line 77
  25. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_3 line 79
  26. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_4 line 81
  27. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_5 line 83
  28. def OAI.MUB6.Certificate.GramEntries.Block5.entry6_6 line 85
  29. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_0 line 87
  30. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_1 line 89
  31. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_2 line 91
  32. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_3 line 93
  33. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_4 line 95
  34. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_5 line 97
  35. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_6 line 99
  36. def OAI.MUB6.Certificate.GramEntries.Block5.entry7_7 line 101
  37. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_0 line 103
  38. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_1 line 105
  39. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_2 line 107
  40. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_3 line 109
  41. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_4 line 111
  42. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_5 line 113
  43. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_6 line 115
  44. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_7 line 117
  45. def OAI.MUB6.Certificate.GramEntries.Block5.entry8_8 line 119
  46. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_0 line 121
  47. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_1 line 123
  48. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_2 line 125
  49. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_3 line 127
  50. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_4 line 129
  51. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_5 line 131
  52. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_6 line 133
  53. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_7 line 135
  54. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_8 line 137
  55. def OAI.MUB6.Certificate.GramEntries.Block5.entry9_9 line 139
  56. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_0 line 141
  57. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_1 line 143
  58. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_2 line 145
  59. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_3 line 147
  60. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_4 line 149
  61. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_5 line 151
  62. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_6 line 153
  63. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_7 line 155
  64. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_8 line 157
  65. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_9 line 159
  66. def OAI.MUB6.Certificate.GramEntries.Block5.entry10_10 line 161
  67. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_0 line 163
  68. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_1 line 165
  69. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_2 line 167
  70. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_3 line 169
  71. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_4 line 171
  72. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_5 line 173
  73. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_6 line 175
  74. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_7 line 177
  75. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_8 line 179
  76. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_9 line 181
  77. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_10 line 183
  78. def OAI.MUB6.Certificate.GramEntries.Block5.entry11_11 line 185
  79. def OAI.MUB6.Certificate.GramEntries.Block5.entries line 187