OAI/Analysis/MutuallyUnbiased/GramEntries/Block2Data.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

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