OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge46.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined368_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined368_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined368_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined368_part3 line 14
  5. def OAI.MUB6.TaoCertificate.combined368_part4 line 16
  6. def OAI.MUB6.TaoCertificate.combined368_part5 line 18
  7. def OAI.MUB6.TaoCertificate.combined368 line 20
  8. theorem OAI.MUB6.TaoCertificate.combined368_checked line 22
  9. theorem OAI.MUB6.TaoCertificate.combined368_zero line 25
  10. def OAI.MUB6.TaoCertificate.combined369_part0 line 33
  11. def OAI.MUB6.TaoCertificate.combined369_part1 line 35
  12. def OAI.MUB6.TaoCertificate.combined369_part2 line 37
  13. def OAI.MUB6.TaoCertificate.combined369_part3 line 39
  14. def OAI.MUB6.TaoCertificate.combined369_part4 line 41
  15. def OAI.MUB6.TaoCertificate.combined369_part5 line 43
  16. def OAI.MUB6.TaoCertificate.combined369_part6 line 45
  17. def OAI.MUB6.TaoCertificate.combined369 line 47
  18. theorem OAI.MUB6.TaoCertificate.combined369_checked line 49
  19. theorem OAI.MUB6.TaoCertificate.combined369_zero line 52
  20. def OAI.MUB6.TaoCertificate.combined370_part0 line 60
  21. def OAI.MUB6.TaoCertificate.combined370_part1 line 62
  22. def OAI.MUB6.TaoCertificate.combined370_part2 line 64
  23. def OAI.MUB6.TaoCertificate.combined370_part3 line 66
  24. def OAI.MUB6.TaoCertificate.combined370_part4 line 68
  25. def OAI.MUB6.TaoCertificate.combined370_part5 line 70
  26. def OAI.MUB6.TaoCertificate.combined370_part6 line 72
  27. def OAI.MUB6.TaoCertificate.combined370 line 74
  28. theorem OAI.MUB6.TaoCertificate.combined370_checked line 76
  29. theorem OAI.MUB6.TaoCertificate.combined370_zero line 79
  30. def OAI.MUB6.TaoCertificate.combined371_part0 line 87
  31. def OAI.MUB6.TaoCertificate.combined371_part1 line 89
  32. def OAI.MUB6.TaoCertificate.combined371_part2 line 91
  33. def OAI.MUB6.TaoCertificate.combined371_part3 line 93
  34. def OAI.MUB6.TaoCertificate.combined371_part4 line 95
  35. def OAI.MUB6.TaoCertificate.combined371_part5 line 97
  36. def OAI.MUB6.TaoCertificate.combined371_part6 line 99
  37. def OAI.MUB6.TaoCertificate.combined371_part7 line 101
  38. def OAI.MUB6.TaoCertificate.combined371 line 103
  39. theorem OAI.MUB6.TaoCertificate.combined371_checked line 105
  40. theorem OAI.MUB6.TaoCertificate.combined371_zero line 108
  41. def OAI.MUB6.TaoCertificate.combined372_part0 line 116
  42. def OAI.MUB6.TaoCertificate.combined372_part1 line 118
  43. def OAI.MUB6.TaoCertificate.combined372_part2 line 120
  44. def OAI.MUB6.TaoCertificate.combined372_part3 line 122
  45. def OAI.MUB6.TaoCertificate.combined372_part4 line 124
  46. def OAI.MUB6.TaoCertificate.combined372_part5 line 126
  47. def OAI.MUB6.TaoCertificate.combined372_part6 line 128
  48. def OAI.MUB6.TaoCertificate.combined372_part7 line 130
  49. def OAI.MUB6.TaoCertificate.combined372 line 132
  50. theorem OAI.MUB6.TaoCertificate.combined372_checked line 134
  51. theorem OAI.MUB6.TaoCertificate.combined372_zero line 137
  52. def OAI.MUB6.TaoCertificate.combined373_part0 line 145
  53. def OAI.MUB6.TaoCertificate.combined373_part1 line 147
  54. def OAI.MUB6.TaoCertificate.combined373_part2 line 149
  55. def OAI.MUB6.TaoCertificate.combined373_part3 line 151
  56. def OAI.MUB6.TaoCertificate.combined373_part4 line 153
  57. def OAI.MUB6.TaoCertificate.combined373_part5 line 155
  58. def OAI.MUB6.TaoCertificate.combined373_part6 line 157
  59. def OAI.MUB6.TaoCertificate.combined373_part7 line 159
  60. def OAI.MUB6.TaoCertificate.combined373_part8 line 161
  61. def OAI.MUB6.TaoCertificate.combined373 line 163
  62. theorem OAI.MUB6.TaoCertificate.combined373_checked line 165
  63. theorem OAI.MUB6.TaoCertificate.combined373_zero line 168
  64. def OAI.MUB6.TaoCertificate.combined374_part0 line 176
  65. def OAI.MUB6.TaoCertificate.combined374_part1 line 178
  66. def OAI.MUB6.TaoCertificate.combined374_part2 line 180
  67. def OAI.MUB6.TaoCertificate.combined374_part3 line 182
  68. def OAI.MUB6.TaoCertificate.combined374_part4 line 184
  69. def OAI.MUB6.TaoCertificate.combined374_part5 line 186
  70. def OAI.MUB6.TaoCertificate.combined374_part6 line 188
  71. def OAI.MUB6.TaoCertificate.combined374_part7 line 190
  72. def OAI.MUB6.TaoCertificate.combined374_part8 line 192
  73. def OAI.MUB6.TaoCertificate.combined374 line 194
  74. theorem OAI.MUB6.TaoCertificate.combined374_checked line 196
  75. theorem OAI.MUB6.TaoCertificate.combined374_zero line 199
  76. def OAI.MUB6.TaoCertificate.combined375_part0 line 207
  77. def OAI.MUB6.TaoCertificate.combined375_part1 line 209
  78. def OAI.MUB6.TaoCertificate.combined375_part2 line 211
  79. def OAI.MUB6.TaoCertificate.combined375_part3 line 213
  80. def OAI.MUB6.TaoCertificate.combined375_part4 line 215
  81. def OAI.MUB6.TaoCertificate.combined375_part5 line 217
  82. def OAI.MUB6.TaoCertificate.combined375_part6 line 219
  83. def OAI.MUB6.TaoCertificate.combined375_part7 line 221
  84. def OAI.MUB6.TaoCertificate.combined375_part8 line 223
  85. def OAI.MUB6.TaoCertificate.combined375 line 225
  86. theorem OAI.MUB6.TaoCertificate.combined375_checked line 227
  87. theorem OAI.MUB6.TaoCertificate.combined375_zero line 230