OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical270.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8640 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8640step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8640 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8641 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw8641step0 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8641 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw8642 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw8642step0 line 47
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8642 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw8643 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw8643step0 line 60
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8643 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw8644 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw8644step0 line 73
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8644 line 75
  16. def OAI.MUB6.Certificate.PairSemantics.raw8645 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw8645step0 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8645 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw8646 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw8646step0 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw8646step1 line 101
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8646 line 103
  23. def OAI.MUB6.Certificate.PairSemantics.raw8647 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw8647step0 line 119
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8647 line 121
  26. def OAI.MUB6.Certificate.PairSemantics.raw8648 line 130
  27. def OAI.MUB6.Certificate.PairSemantics.raw8648step0 line 132
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8648 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw8649 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw8649step0 line 145
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8649 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw8650 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw8650step0 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw8650step1 line 160
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8650 line 162
  36. def OAI.MUB6.Certificate.PairSemantics.raw8651 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw8651step0 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8651 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw8652 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw8652step0 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8652 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw8653 line 202
  43. def OAI.MUB6.Certificate.PairSemantics.raw8653step0 line 204
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8653 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw8654 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw8654step0 line 217
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8654 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw8655 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw8655step0 line 230
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8655 line 232
  51. def OAI.MUB6.Certificate.PairSemantics.raw8656 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw8656step0 line 243
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8656 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw8657 line 254
  55. def OAI.MUB6.Certificate.PairSemantics.raw8657step0 line 256
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8657 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw8658 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw8658step0 line 269
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8658 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw8659 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw8659step0 line 282
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8659 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw8660 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw8660step0 line 295
  65. def OAI.MUB6.Certificate.PairSemantics.raw8660step1 line 297
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8660 line 299
  67. def OAI.MUB6.Certificate.PairSemantics.raw8661 line 313
  68. def OAI.MUB6.Certificate.PairSemantics.raw8661step0 line 315
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8661 line 317
  70. def OAI.MUB6.Certificate.PairSemantics.raw8662 line 326
  71. def OAI.MUB6.Certificate.PairSemantics.raw8662step0 line 328
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8662 line 330
  73. def OAI.MUB6.Certificate.PairSemantics.raw8663 line 339
  74. def OAI.MUB6.Certificate.PairSemantics.raw8663step0 line 341
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8663 line 343
  76. def OAI.MUB6.Certificate.PairSemantics.raw8664 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw8664step0 line 354
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8664 line 356
  79. def OAI.MUB6.Certificate.PairSemantics.raw8665 line 365
  80. def OAI.MUB6.Certificate.PairSemantics.raw8665step0 line 367
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8665 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw8666 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw8666step0 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw8666step1 line 382
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8666 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw8667 line 397
  87. def OAI.MUB6.Certificate.PairSemantics.raw8667step0 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw8667step1 line 401
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8667 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw8668 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw8668step0 line 418
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8668 line 420
  93. def OAI.MUB6.Certificate.PairSemantics.raw8669 line 429
  94. def OAI.MUB6.Certificate.PairSemantics.raw8669step0 line 431
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical8669 line 433
  96. def OAI.MUB6.Certificate.PairSemantics.raw8670 line 442
  97. def OAI.MUB6.Certificate.PairSemantics.raw8670step0 line 444
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8670 line 446
  99. def OAI.MUB6.Certificate.PairSemantics.raw8671 line 455
  100. def OAI.MUB6.Certificate.PairSemantics.raw8671step0 line 457
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8671 line 459