OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical74.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2368 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw2368step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2368 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw2369 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw2369step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2369 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw2370 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2370 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw2371 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2371 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw2372 line 53
  12. def OAI.MUB6.Certificate.PairSemantics.raw2372step0 line 55
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2372 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw2373 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw2373step0 line 68
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2373 line 70
  17. def OAI.MUB6.Certificate.PairSemantics.raw2374 line 79
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2374 line 81
  19. def OAI.MUB6.Certificate.PairSemantics.raw2375 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw2375step0 line 87
  21. def OAI.MUB6.Certificate.PairSemantics.raw2375step1 line 89
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2375 line 91
  23. def OAI.MUB6.Certificate.PairSemantics.raw2376 line 104
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2376 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw2377 line 110
  26. def OAI.MUB6.Certificate.PairSemantics.raw2377step0 line 112
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2377 line 114
  28. def OAI.MUB6.Certificate.PairSemantics.raw2378 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw2378step0 line 125
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2378 line 127
  31. def OAI.MUB6.Certificate.PairSemantics.raw2379 line 136
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2379 line 138
  33. def OAI.MUB6.Certificate.PairSemantics.raw2380 line 142
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2380 line 144
  35. def OAI.MUB6.Certificate.PairSemantics.raw2381 line 148
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2381 line 150
  37. def OAI.MUB6.Certificate.PairSemantics.raw2382 line 154
  38. def OAI.MUB6.Certificate.PairSemantics.raw2382step0 line 156
  39. def OAI.MUB6.Certificate.PairSemantics.raw2382step1 line 158
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2382 line 160
  41. def OAI.MUB6.Certificate.PairSemantics.raw2383 line 173
  42. def OAI.MUB6.Certificate.PairSemantics.raw2383step0 line 175
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2383 line 177
  44. def OAI.MUB6.Certificate.PairSemantics.raw2384 line 186
  45. def OAI.MUB6.Certificate.PairSemantics.raw2384step0 line 188
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2384 line 190
  47. def OAI.MUB6.Certificate.PairSemantics.raw2385 line 199
  48. def OAI.MUB6.Certificate.PairSemantics.raw2385step0 line 201
  49. def OAI.MUB6.Certificate.PairSemantics.raw2385step1 line 203
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2385 line 205
  51. def OAI.MUB6.Certificate.PairSemantics.raw2386 line 218
  52. def OAI.MUB6.Certificate.PairSemantics.raw2386step0 line 220
  53. def OAI.MUB6.Certificate.PairSemantics.raw2386step1 line 222
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2386 line 224
  55. def OAI.MUB6.Certificate.PairSemantics.raw2387 line 237
  56. def OAI.MUB6.Certificate.PairSemantics.raw2387step0 line 239
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2387 line 241
  58. def OAI.MUB6.Certificate.PairSemantics.raw2388 line 250
  59. def OAI.MUB6.Certificate.PairSemantics.raw2388step0 line 252
  60. def OAI.MUB6.Certificate.PairSemantics.raw2388step1 line 254
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2388 line 256
  62. def OAI.MUB6.Certificate.PairSemantics.raw2389 line 269
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2389 line 271
  64. def OAI.MUB6.Certificate.PairSemantics.raw2390 line 275
  65. def OAI.MUB6.Certificate.PairSemantics.raw2390step0 line 277
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2390 line 279
  67. def OAI.MUB6.Certificate.PairSemantics.raw2391 line 288
  68. def OAI.MUB6.Certificate.PairSemantics.raw2391step0 line 290
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2391 line 292
  70. def OAI.MUB6.Certificate.PairSemantics.raw2392 line 301
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2392 line 303
  72. def OAI.MUB6.Certificate.PairSemantics.raw2393 line 307
  73. def OAI.MUB6.Certificate.PairSemantics.raw2393step0 line 309
  74. def OAI.MUB6.Certificate.PairSemantics.raw2393step1 line 311
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2393 line 313
  76. def OAI.MUB6.Certificate.PairSemantics.raw2394 line 326
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2394 line 328
  78. def OAI.MUB6.Certificate.PairSemantics.raw2395 line 332
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2395 line 334
  80. def OAI.MUB6.Certificate.PairSemantics.raw2396 line 338
  81. def OAI.MUB6.Certificate.PairSemantics.raw2396step0 line 340
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2396 line 342
  83. def OAI.MUB6.Certificate.PairSemantics.raw2397 line 351
  84. def OAI.MUB6.Certificate.PairSemantics.raw2397step0 line 353
  85. def OAI.MUB6.Certificate.PairSemantics.raw2397step1 line 355
  86. def OAI.MUB6.Certificate.PairSemantics.raw2397step2 line 357
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2397 line 359
  88. def OAI.MUB6.Certificate.PairSemantics.raw2398 line 376
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2398 line 378
  90. def OAI.MUB6.Certificate.PairSemantics.raw2399 line 382
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2399 line 384