OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical199.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6368 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw6368step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6368 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw6369 line 32
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6369 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw6370 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw6370step0 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw6370step1 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw6370step2 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6370 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw6371 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw6371step0 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw6371step1 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6371 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw6372 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw6372step0 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw6372step1 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6372 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw6373 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw6373step0 line 103
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6373 line 105
  22. def OAI.MUB6.Certificate.PairSemantics.raw6374 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw6374step0 line 116
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6374 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw6375 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw6375step0 line 129
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6375 line 131
  28. def OAI.MUB6.Certificate.PairSemantics.raw6376 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw6376step0 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw6376step1 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6376 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw6377 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw6377step0 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw6377step1 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw6377step2 line 165
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6377 line 167
  37. def OAI.MUB6.Certificate.PairSemantics.raw6378 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw6378step0 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw6378step1 line 188
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6378 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw6379 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw6379step0 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw6379step1 line 207
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6379 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw6380 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw6380step0 line 224
  47. def OAI.MUB6.Certificate.PairSemantics.raw6380step1 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw6380step2 line 228
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6380 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw6381 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw6381step0 line 249
  52. def OAI.MUB6.Certificate.PairSemantics.raw6381step1 line 251
  53. def OAI.MUB6.Certificate.PairSemantics.raw6381step2 line 253
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6381 line 255
  55. def OAI.MUB6.Certificate.PairSemantics.raw6382 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw6382step0 line 274
  57. def OAI.MUB6.Certificate.PairSemantics.raw6382step1 line 276
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6382 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw6383 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw6383step0 line 293
  61. def OAI.MUB6.Certificate.PairSemantics.raw6383step1 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6383 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw6384 line 310
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6384 line 312
  65. def OAI.MUB6.Certificate.PairSemantics.raw6385 line 316
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6385 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw6386 line 322
  68. def OAI.MUB6.Certificate.PairSemantics.raw6386step0 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw6386step1 line 326
  70. def OAI.MUB6.Certificate.PairSemantics.raw6386step2 line 328
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6386 line 330
  72. def OAI.MUB6.Certificate.PairSemantics.raw6387 line 347
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6387 line 349
  74. def OAI.MUB6.Certificate.PairSemantics.raw6388 line 353
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6388 line 355
  76. def OAI.MUB6.Certificate.PairSemantics.raw6389 line 359
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6389 line 361
  78. def OAI.MUB6.Certificate.PairSemantics.raw6390 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw6390step0 line 367
  80. def OAI.MUB6.Certificate.PairSemantics.raw6390step1 line 369
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6390 line 371
  82. def OAI.MUB6.Certificate.PairSemantics.raw6391 line 384
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6391 line 386
  84. def OAI.MUB6.Certificate.PairSemantics.raw6392 line 390
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6392 line 392
  86. def OAI.MUB6.Certificate.PairSemantics.raw6393 line 396
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6393 line 398
  88. def OAI.MUB6.Certificate.PairSemantics.raw6394 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw6394step0 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw6394step1 line 406
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6394 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw6395 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw6395step0 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw6395step1 line 425
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6395 line 427
  96. def OAI.MUB6.Certificate.PairSemantics.raw6396 line 440
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical6396 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw6397 line 446
  99. def OAI.MUB6.Certificate.PairSemantics.raw6397step0 line 448
  100. def OAI.MUB6.Certificate.PairSemantics.raw6397step1 line 450
  101. def OAI.MUB6.Certificate.PairSemantics.raw6397step2 line 452
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical6397 line 454
  103. def OAI.MUB6.Certificate.PairSemantics.raw6398 line 471
  104. def OAI.MUB6.Certificate.PairSemantics.raw6398step0 line 473
  105. def OAI.MUB6.Certificate.PairSemantics.raw6398step1 line 475
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical6398 line 477
  107. def OAI.MUB6.Certificate.PairSemantics.raw6399 line 490
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6399 line 492