OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical168.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5376 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw5376step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw5376step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5376 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw5377 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw5377step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw5377step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5377 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw5378 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw5378step0 line 61
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5378 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw5379 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw5379step0 line 74
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5379 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw5380 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw5380step0 line 87
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5380 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw5381 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw5381step0 line 100
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5381 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw5382 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw5382step0 line 113
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical5382 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw5383 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw5383step0 line 126
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5383 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw5384 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw5384step0 line 139
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5384 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw5385 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw5385step0 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw5385step1 line 154
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5385 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw5386 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw5386step0 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5386 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw5387 line 182
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5387 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw5388 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw5388step0 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw5388step1 line 192
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5388 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw5389 line 207
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5389 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw5390 line 213
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5390 line 215
  47. def OAI.MUB6.Certificate.PairSemantics.raw5391 line 219
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5391 line 221
  49. def OAI.MUB6.Certificate.PairSemantics.raw5392 line 225
  50. def OAI.MUB6.Certificate.PairSemantics.raw5392step0 line 227
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5392 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw5393 line 238
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5393 line 240
  54. def OAI.MUB6.Certificate.PairSemantics.raw5394 line 244
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5394 line 246
  56. def OAI.MUB6.Certificate.PairSemantics.raw5395 line 250
  57. def OAI.MUB6.Certificate.PairSemantics.raw5395step0 line 252
  58. def OAI.MUB6.Certificate.PairSemantics.raw5395step1 line 254
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5395 line 256
  60. def OAI.MUB6.Certificate.PairSemantics.raw5396 line 269
  61. def OAI.MUB6.Certificate.PairSemantics.raw5396step0 line 271
  62. def OAI.MUB6.Certificate.PairSemantics.raw5396step1 line 273
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5396 line 275
  64. def OAI.MUB6.Certificate.PairSemantics.raw5397 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw5397step0 line 290
  66. def OAI.MUB6.Certificate.PairSemantics.raw5397step1 line 292
  67. def OAI.MUB6.Certificate.PairSemantics.raw5397step2 line 294
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5397 line 296
  69. def OAI.MUB6.Certificate.PairSemantics.raw5398 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw5398step0 line 315
  71. def OAI.MUB6.Certificate.PairSemantics.raw5398step1 line 317
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5398 line 319
  73. def OAI.MUB6.Certificate.PairSemantics.raw5399 line 332
  74. def OAI.MUB6.Certificate.PairSemantics.raw5399step0 line 334
  75. def OAI.MUB6.Certificate.PairSemantics.raw5399step1 line 336
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5399 line 338
  77. def OAI.MUB6.Certificate.PairSemantics.raw5400 line 351
  78. def OAI.MUB6.Certificate.PairSemantics.raw5400step0 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw5400step1 line 355
  80. def OAI.MUB6.Certificate.PairSemantics.raw5400step2 line 357
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5400 line 359
  82. def OAI.MUB6.Certificate.PairSemantics.raw5401 line 376
  83. def OAI.MUB6.Certificate.PairSemantics.raw5401step0 line 378
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5401 line 380
  85. def OAI.MUB6.Certificate.PairSemantics.raw5402 line 389
  86. def OAI.MUB6.Certificate.PairSemantics.raw5402step0 line 391
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5402 line 393
  88. def OAI.MUB6.Certificate.PairSemantics.raw5403 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw5403step0 line 404
  90. def OAI.MUB6.Certificate.PairSemantics.raw5403step1 line 406
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5403 line 408
  92. def OAI.MUB6.Certificate.PairSemantics.raw5404 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw5404step0 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw5404step1 line 425
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical5404 line 427
  96. def OAI.MUB6.Certificate.PairSemantics.raw5405 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw5405step0 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw5405step1 line 444
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5405 line 446
  100. def OAI.MUB6.Certificate.PairSemantics.raw5406 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw5406step0 line 461
  102. def OAI.MUB6.Certificate.PairSemantics.raw5406step1 line 463
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5406 line 465
  104. def OAI.MUB6.Certificate.PairSemantics.raw5407 line 478
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical5407 line 480