OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge47.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined376_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined376_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined376_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined376_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined376_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined376_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined376_part6 line 20
  8. def OAI.MUB6.TaoCertificate.combined376_part7 line 22
  9. def OAI.MUB6.TaoCertificate.combined376_part8 line 24
  10. def OAI.MUB6.TaoCertificate.combined376_part9 line 26
  11. def OAI.MUB6.TaoCertificate.combined376 line 28
  12. theorem OAI.MUB6.TaoCertificate.combined376_checked line 30
  13. theorem OAI.MUB6.TaoCertificate.combined376_zero line 33
  14. def OAI.MUB6.TaoCertificate.combined377_part0 line 41
  15. def OAI.MUB6.TaoCertificate.combined377_part1 line 43
  16. def OAI.MUB6.TaoCertificate.combined377_part2 line 45
  17. def OAI.MUB6.TaoCertificate.combined377_part3 line 47
  18. def OAI.MUB6.TaoCertificate.combined377_part4 line 49
  19. def OAI.MUB6.TaoCertificate.combined377_part5 line 51
  20. def OAI.MUB6.TaoCertificate.combined377_part6 line 53
  21. def OAI.MUB6.TaoCertificate.combined377_part7 line 55
  22. def OAI.MUB6.TaoCertificate.combined377_part8 line 57
  23. def OAI.MUB6.TaoCertificate.combined377_part9 line 59
  24. def OAI.MUB6.TaoCertificate.combined377 line 61
  25. theorem OAI.MUB6.TaoCertificate.combined377_checked line 63
  26. theorem OAI.MUB6.TaoCertificate.combined377_zero line 66
  27. def OAI.MUB6.TaoCertificate.combined378_part0 line 74
  28. def OAI.MUB6.TaoCertificate.combined378_part1 line 76
  29. def OAI.MUB6.TaoCertificate.combined378_part2 line 78
  30. def OAI.MUB6.TaoCertificate.combined378_part3 line 80
  31. def OAI.MUB6.TaoCertificate.combined378_part4 line 82
  32. def OAI.MUB6.TaoCertificate.combined378_part5 line 84
  33. def OAI.MUB6.TaoCertificate.combined378_part6 line 86
  34. def OAI.MUB6.TaoCertificate.combined378_part7 line 88
  35. def OAI.MUB6.TaoCertificate.combined378_part8 line 90
  36. def OAI.MUB6.TaoCertificate.combined378_part9 line 92
  37. def OAI.MUB6.TaoCertificate.combined378 line 94
  38. theorem OAI.MUB6.TaoCertificate.combined378_checked line 96
  39. theorem OAI.MUB6.TaoCertificate.combined378_zero line 99
  40. def OAI.MUB6.TaoCertificate.combined379_part0 line 107
  41. def OAI.MUB6.TaoCertificate.combined379_part1 line 109
  42. def OAI.MUB6.TaoCertificate.combined379_part2 line 111
  43. def OAI.MUB6.TaoCertificate.combined379_part3 line 113
  44. def OAI.MUB6.TaoCertificate.combined379_part4 line 115
  45. def OAI.MUB6.TaoCertificate.combined379_part5 line 117
  46. def OAI.MUB6.TaoCertificate.combined379_part6 line 119
  47. def OAI.MUB6.TaoCertificate.combined379_part7 line 121
  48. def OAI.MUB6.TaoCertificate.combined379_part8 line 123
  49. def OAI.MUB6.TaoCertificate.combined379_part9 line 125
  50. def OAI.MUB6.TaoCertificate.combined379_part10 line 127
  51. def OAI.MUB6.TaoCertificate.combined379 line 129
  52. theorem OAI.MUB6.TaoCertificate.combined379_checked line 131
  53. theorem OAI.MUB6.TaoCertificate.combined379_zero line 134
  54. def OAI.MUB6.TaoCertificate.combined380_part0 line 142
  55. def OAI.MUB6.TaoCertificate.combined380_part1 line 144
  56. def OAI.MUB6.TaoCertificate.combined380_part2 line 146
  57. def OAI.MUB6.TaoCertificate.combined380_part3 line 148
  58. def OAI.MUB6.TaoCertificate.combined380_part4 line 150
  59. def OAI.MUB6.TaoCertificate.combined380_part5 line 152
  60. def OAI.MUB6.TaoCertificate.combined380_part6 line 154
  61. def OAI.MUB6.TaoCertificate.combined380_part7 line 156
  62. def OAI.MUB6.TaoCertificate.combined380_part8 line 158
  63. def OAI.MUB6.TaoCertificate.combined380_part9 line 160
  64. def OAI.MUB6.TaoCertificate.combined380_part10 line 162
  65. def OAI.MUB6.TaoCertificate.combined380 line 164
  66. theorem OAI.MUB6.TaoCertificate.combined380_checked line 166
  67. theorem OAI.MUB6.TaoCertificate.combined380_zero line 169
  68. def OAI.MUB6.TaoCertificate.combined381_part0 line 177
  69. def OAI.MUB6.TaoCertificate.combined381_part1 line 179
  70. def OAI.MUB6.TaoCertificate.combined381_part2 line 181
  71. def OAI.MUB6.TaoCertificate.combined381_part3 line 183
  72. def OAI.MUB6.TaoCertificate.combined381_part4 line 185
  73. def OAI.MUB6.TaoCertificate.combined381_part5 line 187
  74. def OAI.MUB6.TaoCertificate.combined381_part6 line 189
  75. def OAI.MUB6.TaoCertificate.combined381_part7 line 191
  76. def OAI.MUB6.TaoCertificate.combined381_part8 line 193
  77. def OAI.MUB6.TaoCertificate.combined381_part9 line 195
  78. def OAI.MUB6.TaoCertificate.combined381_part10 line 197
  79. def OAI.MUB6.TaoCertificate.combined381 line 199
  80. theorem OAI.MUB6.TaoCertificate.combined381_checked line 201
  81. theorem OAI.MUB6.TaoCertificate.combined381_zero line 204
  82. def OAI.MUB6.TaoCertificate.combined382_part0 line 212
  83. def OAI.MUB6.TaoCertificate.combined382_part1 line 214
  84. def OAI.MUB6.TaoCertificate.combined382_part2 line 216
  85. def OAI.MUB6.TaoCertificate.combined382_part3 line 218
  86. def OAI.MUB6.TaoCertificate.combined382_part4 line 220
  87. def OAI.MUB6.TaoCertificate.combined382_part5 line 222
  88. def OAI.MUB6.TaoCertificate.combined382_part6 line 224
  89. def OAI.MUB6.TaoCertificate.combined382_part7 line 226
  90. def OAI.MUB6.TaoCertificate.combined382_part8 line 228
  91. def OAI.MUB6.TaoCertificate.combined382_part9 line 230
  92. def OAI.MUB6.TaoCertificate.combined382_part10 line 232
  93. def OAI.MUB6.TaoCertificate.combined382_part11 line 234
  94. def OAI.MUB6.TaoCertificate.combined382 line 236
  95. theorem OAI.MUB6.TaoCertificate.combined382_checked line 238
  96. theorem OAI.MUB6.TaoCertificate.combined382_zero line 241
  97. def OAI.MUB6.TaoCertificate.combined383_part0 line 249
  98. def OAI.MUB6.TaoCertificate.combined383_part1 line 251
  99. def OAI.MUB6.TaoCertificate.combined383_part2 line 253
  100. def OAI.MUB6.TaoCertificate.combined383_part3 line 255
  101. def OAI.MUB6.TaoCertificate.combined383_part4 line 257
  102. def OAI.MUB6.TaoCertificate.combined383_part5 line 259
  103. def OAI.MUB6.TaoCertificate.combined383_part6 line 261
  104. def OAI.MUB6.TaoCertificate.combined383_part7 line 263
  105. def OAI.MUB6.TaoCertificate.combined383_part8 line 265
  106. def OAI.MUB6.TaoCertificate.combined383_part9 line 267
  107. def OAI.MUB6.TaoCertificate.combined383_part10 line 269
  108. def OAI.MUB6.TaoCertificate.combined383_part11 line 271
  109. def OAI.MUB6.TaoCertificate.combined383 line 273
  110. theorem OAI.MUB6.TaoCertificate.combined383_checked line 275
  111. theorem OAI.MUB6.TaoCertificate.combined383_zero line 278