OAI/Analysis/MutuallyUnbiased/GramKeys/Block24.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramRows.key3072 line 9
  2. def OAI.MUB6.Certificate.GramRows.key3073 line 10
  3. def OAI.MUB6.Certificate.GramRows.key3074 line 11
  4. def OAI.MUB6.Certificate.GramRows.key3075 line 12
  5. def OAI.MUB6.Certificate.GramRows.key3076 line 13
  6. def OAI.MUB6.Certificate.GramRows.key3077 line 14
  7. def OAI.MUB6.Certificate.GramRows.key3078 line 15
  8. def OAI.MUB6.Certificate.GramRows.key3079 line 16
  9. def OAI.MUB6.Certificate.GramRows.key3080 line 17
  10. def OAI.MUB6.Certificate.GramRows.key3081 line 18
  11. def OAI.MUB6.Certificate.GramRows.key3082 line 19
  12. def OAI.MUB6.Certificate.GramRows.key3083 line 20
  13. def OAI.MUB6.Certificate.GramRows.key3084 line 21
  14. def OAI.MUB6.Certificate.GramRows.key3085 line 22
  15. def OAI.MUB6.Certificate.GramRows.key3086 line 23
  16. def OAI.MUB6.Certificate.GramRows.key3087 line 24
  17. def OAI.MUB6.Certificate.GramRows.key3088 line 25
  18. def OAI.MUB6.Certificate.GramRows.key3089 line 26
  19. def OAI.MUB6.Certificate.GramRows.key3090 line 27
  20. def OAI.MUB6.Certificate.GramRows.key3091 line 28
  21. def OAI.MUB6.Certificate.GramRows.key3092 line 29
  22. def OAI.MUB6.Certificate.GramRows.key3093 line 30
  23. def OAI.MUB6.Certificate.GramRows.key3094 line 31
  24. def OAI.MUB6.Certificate.GramRows.key3095 line 32
  25. def OAI.MUB6.Certificate.GramRows.key3096 line 33
  26. def OAI.MUB6.Certificate.GramRows.key3097 line 34
  27. def OAI.MUB6.Certificate.GramRows.key3098 line 35
  28. def OAI.MUB6.Certificate.GramRows.key3099 line 36
  29. def OAI.MUB6.Certificate.GramRows.key3100 line 37
  30. def OAI.MUB6.Certificate.GramRows.key3101 line 38
  31. def OAI.MUB6.Certificate.GramRows.key3102 line 39
  32. def OAI.MUB6.Certificate.GramRows.key3103 line 40
  33. def OAI.MUB6.Certificate.GramRows.key3104 line 41
  34. def OAI.MUB6.Certificate.GramRows.key3105 line 42
  35. def OAI.MUB6.Certificate.GramRows.key3106 line 43
  36. def OAI.MUB6.Certificate.GramRows.key3107 line 44
  37. def OAI.MUB6.Certificate.GramRows.key3108 line 45
  38. def OAI.MUB6.Certificate.GramRows.key3109 line 46
  39. def OAI.MUB6.Certificate.GramRows.key3110 line 47
  40. def OAI.MUB6.Certificate.GramRows.key3111 line 48
  41. def OAI.MUB6.Certificate.GramRows.key3112 line 49
  42. def OAI.MUB6.Certificate.GramRows.key3113 line 50
  43. def OAI.MUB6.Certificate.GramRows.key3114 line 51
  44. def OAI.MUB6.Certificate.GramRows.key3115 line 52
  45. def OAI.MUB6.Certificate.GramRows.key3116 line 53
  46. def OAI.MUB6.Certificate.GramRows.key3117 line 54
  47. def OAI.MUB6.Certificate.GramRows.key3118 line 55
  48. def OAI.MUB6.Certificate.GramRows.key3119 line 56
  49. def OAI.MUB6.Certificate.GramRows.key3120 line 57
  50. def OAI.MUB6.Certificate.GramRows.key3121 line 58
  51. def OAI.MUB6.Certificate.GramRows.key3122 line 59
  52. def OAI.MUB6.Certificate.GramRows.key3123 line 60
  53. def OAI.MUB6.Certificate.GramRows.key3124 line 61
  54. def OAI.MUB6.Certificate.GramRows.key3125 line 62
  55. def OAI.MUB6.Certificate.GramRows.key3126 line 63
  56. def OAI.MUB6.Certificate.GramRows.key3127 line 64
  57. def OAI.MUB6.Certificate.GramRows.key3128 line 65
  58. def OAI.MUB6.Certificate.GramRows.key3129 line 66
  59. def OAI.MUB6.Certificate.GramRows.key3130 line 67
  60. def OAI.MUB6.Certificate.GramRows.key3131 line 68
  61. def OAI.MUB6.Certificate.GramRows.key3132 line 69
  62. def OAI.MUB6.Certificate.GramRows.key3133 line 70
  63. def OAI.MUB6.Certificate.GramRows.key3134 line 71
  64. def OAI.MUB6.Certificate.GramRows.key3135 line 72
  65. def OAI.MUB6.Certificate.GramRows.key3136 line 73
  66. def OAI.MUB6.Certificate.GramRows.key3137 line 74
  67. def OAI.MUB6.Certificate.GramRows.key3138 line 75
  68. def OAI.MUB6.Certificate.GramRows.key3139 line 76
  69. def OAI.MUB6.Certificate.GramRows.key3140 line 77
  70. def OAI.MUB6.Certificate.GramRows.key3141 line 78
  71. def OAI.MUB6.Certificate.GramRows.key3142 line 79
  72. def OAI.MUB6.Certificate.GramRows.key3143 line 80
  73. def OAI.MUB6.Certificate.GramRows.key3144 line 81
  74. def OAI.MUB6.Certificate.GramRows.key3145 line 82
  75. def OAI.MUB6.Certificate.GramRows.key3146 line 83
  76. def OAI.MUB6.Certificate.GramRows.key3147 line 84
  77. def OAI.MUB6.Certificate.GramRows.key3148 line 85