OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical298.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9536 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw9536step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw9536step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9536 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw9537 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw9537step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw9537step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9537 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw9538 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw9538step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw9538step1 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9538 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw9539 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw9539step0 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw9539step1 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical9539 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw9540 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw9540step0 line 99
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9540 line 101
  20. def OAI.MUB6.Certificate.PairSemantics.raw9541 line 110
  21. def OAI.MUB6.Certificate.PairSemantics.raw9541step0 line 112
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9541 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw9542 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw9542step0 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw9542step1 line 127
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9542 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw9543 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw9543step0 line 144
  29. def OAI.MUB6.Certificate.PairSemantics.raw9543step1 line 146
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9543 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw9544 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw9544step0 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw9544step1 line 165
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9544 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw9545 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw9545step0 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw9545step1 line 184
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9545 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw9546 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw9546step0 line 201
  41. def OAI.MUB6.Certificate.PairSemantics.raw9546step1 line 203
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9546 line 205
  43. def OAI.MUB6.Certificate.PairSemantics.raw9547 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw9547step0 line 220
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9547 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw9548 line 231
  47. def OAI.MUB6.Certificate.PairSemantics.raw9548step0 line 233
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical9548 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw9549 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw9549step0 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw9549step1 line 248
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9549 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw9550 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw9550step0 line 265
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9550 line 267
  56. def OAI.MUB6.Certificate.PairSemantics.raw9551 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw9551step0 line 278
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9551 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw9552 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw9552step0 line 291
  61. def OAI.MUB6.Certificate.PairSemantics.raw9552step1 line 293
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical9552 line 295
  63. def OAI.MUB6.Certificate.PairSemantics.raw9553 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw9553step0 line 310
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical9553 line 312
  66. def OAI.MUB6.Certificate.PairSemantics.raw9554 line 321
  67. def OAI.MUB6.Certificate.PairSemantics.raw9554step0 line 323
  68. def OAI.MUB6.Certificate.PairSemantics.raw9554step1 line 325
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9554 line 327
  70. def OAI.MUB6.Certificate.PairSemantics.raw9555 line 341
  71. def OAI.MUB6.Certificate.PairSemantics.raw9555step0 line 343
  72. def OAI.MUB6.Certificate.PairSemantics.raw9555step1 line 345
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9555 line 347
  74. def OAI.MUB6.Certificate.PairSemantics.raw9556 line 361
  75. def OAI.MUB6.Certificate.PairSemantics.raw9556step0 line 363
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical9556 line 365
  77. def OAI.MUB6.Certificate.PairSemantics.raw9557 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw9557step0 line 376
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical9557 line 378
  80. def OAI.MUB6.Certificate.PairSemantics.raw9558 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw9558step0 line 389
  82. def OAI.MUB6.Certificate.PairSemantics.raw9558step1 line 391
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9558 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw9559 line 407
  85. def OAI.MUB6.Certificate.PairSemantics.raw9559step0 line 409
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical9559 line 411
  87. def OAI.MUB6.Certificate.PairSemantics.raw9560 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw9560step0 line 422
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9560 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw9561 line 433
  91. def OAI.MUB6.Certificate.PairSemantics.raw9561step0 line 435
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9561 line 437
  93. def OAI.MUB6.Certificate.PairSemantics.raw9562 line 446
  94. def OAI.MUB6.Certificate.PairSemantics.raw9562step0 line 448
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9562 line 450
  96. def OAI.MUB6.Certificate.PairSemantics.raw9563 line 459
  97. def OAI.MUB6.Certificate.PairSemantics.raw9563step0 line 461
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9563 line 463
  99. def OAI.MUB6.Certificate.PairSemantics.raw9564 line 472
  100. def OAI.MUB6.Certificate.PairSemantics.raw9564step0 line 474
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical9564 line 476
  102. def OAI.MUB6.Certificate.PairSemantics.raw9565 line 485
  103. def OAI.MUB6.Certificate.PairSemantics.raw9565step0 line 487
  104. def OAI.MUB6.Certificate.PairSemantics.raw9565step1 line 489
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9565 line 491
  106. def OAI.MUB6.Certificate.PairSemantics.raw9566 line 504
  107. def OAI.MUB6.Certificate.PairSemantics.raw9566step0 line 506
  108. def OAI.MUB6.Certificate.PairSemantics.raw9566step1 line 508
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9566 line 510
  110. def OAI.MUB6.Certificate.PairSemantics.raw9567 line 524
  111. def OAI.MUB6.Certificate.PairSemantics.raw9567step0 line 526
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical9567 line 528