OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical136.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4352 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw4352step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4352 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw4353 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw4353step0 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical4353 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw4354 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw4354step0 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4354 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw4355 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw4355step0 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw4355step1 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw4355step2 line 61
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4355 line 63
  15. def OAI.MUB6.Certificate.PairSemantics.raw4356 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4356 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw4357 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw4357step0 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4357 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw4358 line 100
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4358 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw4359 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4359 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw4360 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw4360step0 line 114
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4360 line 116
  27. def OAI.MUB6.Certificate.PairSemantics.raw4361 line 125
  28. def OAI.MUB6.Certificate.PairSemantics.raw4361step0 line 127
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4361 line 129
  30. def OAI.MUB6.Certificate.PairSemantics.raw4362 line 138
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4362 line 140
  32. def OAI.MUB6.Certificate.PairSemantics.raw4363 line 144
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4363 line 146
  34. def OAI.MUB6.Certificate.PairSemantics.raw4364 line 150
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4364 line 152
  36. def OAI.MUB6.Certificate.PairSemantics.raw4365 line 156
  37. def OAI.MUB6.Certificate.PairSemantics.raw4365step0 line 158
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4365 line 160
  39. def OAI.MUB6.Certificate.PairSemantics.raw4366 line 169
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4366 line 171
  41. def OAI.MUB6.Certificate.PairSemantics.raw4367 line 175
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4367 line 177
  43. def OAI.MUB6.Certificate.PairSemantics.raw4368 line 181
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4368 line 183
  45. def OAI.MUB6.Certificate.PairSemantics.raw4369 line 187
  46. def OAI.MUB6.Certificate.PairSemantics.raw4369step0 line 189
  47. def OAI.MUB6.Certificate.PairSemantics.raw4369step1 line 191
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4369 line 193
  49. def OAI.MUB6.Certificate.PairSemantics.raw4370 line 206
  50. def OAI.MUB6.Certificate.PairSemantics.raw4370step0 line 208
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4370 line 210
  52. def OAI.MUB6.Certificate.PairSemantics.raw4371 line 219
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4371 line 221
  54. def OAI.MUB6.Certificate.PairSemantics.raw4372 line 225
  55. def OAI.MUB6.Certificate.PairSemantics.raw4372step0 line 227
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4372 line 229
  57. def OAI.MUB6.Certificate.PairSemantics.raw4373 line 238
  58. def OAI.MUB6.Certificate.PairSemantics.raw4373step0 line 240
  59. def OAI.MUB6.Certificate.PairSemantics.raw4373step1 line 242
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4373 line 244
  61. def OAI.MUB6.Certificate.PairSemantics.raw4374 line 257
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4374 line 259
  63. def OAI.MUB6.Certificate.PairSemantics.raw4375 line 263
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4375 line 265
  65. def OAI.MUB6.Certificate.PairSemantics.raw4376 line 269
  66. def OAI.MUB6.Certificate.PairSemantics.raw4376step0 line 271
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4376 line 273
  68. def OAI.MUB6.Certificate.PairSemantics.raw4377 line 282
  69. def OAI.MUB6.Certificate.PairSemantics.raw4377step0 line 284
  70. def OAI.MUB6.Certificate.PairSemantics.raw4377step1 line 286
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4377 line 288
  72. def OAI.MUB6.Certificate.PairSemantics.raw4378 line 301
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4378 line 303
  74. def OAI.MUB6.Certificate.PairSemantics.raw4379 line 307
  75. def OAI.MUB6.Certificate.PairSemantics.raw4379step0 line 309
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4379 line 311
  77. def OAI.MUB6.Certificate.PairSemantics.raw4380 line 320
  78. def OAI.MUB6.Certificate.PairSemantics.raw4380step0 line 322
  79. def OAI.MUB6.Certificate.PairSemantics.raw4380step1 line 324
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4380 line 326
  81. def OAI.MUB6.Certificate.PairSemantics.raw4381 line 339
  82. def OAI.MUB6.Certificate.PairSemantics.raw4381step0 line 341
  83. def OAI.MUB6.Certificate.PairSemantics.raw4381step1 line 343
  84. def OAI.MUB6.Certificate.PairSemantics.raw4381step2 line 345
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4381 line 347
  86. def OAI.MUB6.Certificate.PairSemantics.raw4382 line 364
  87. def OAI.MUB6.Certificate.PairSemantics.raw4382step0 line 366
  88. def OAI.MUB6.Certificate.PairSemantics.raw4382step1 line 368
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4382 line 370
  90. def OAI.MUB6.Certificate.PairSemantics.raw4383 line 383
  91. def OAI.MUB6.Certificate.PairSemantics.raw4383step0 line 385
  92. def OAI.MUB6.Certificate.PairSemantics.raw4383step1 line 387
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4383 line 389