OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical128.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4096 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw4096step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw4096step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4096 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw4097 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw4097step0 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw4097step1 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw4097step2 line 40
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4097 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw4098 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw4098step0 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw4098step1 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4098 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw4099 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw4099step0 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4099 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw4100 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw4100step0 line 96
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4100 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw4101 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw4101step0 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw4101step1 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw4101step2 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw4101step3 line 116
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4101 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw4102 line 140
  27. def OAI.MUB6.Certificate.PairSemantics.raw4102step0 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw4102step1 line 144
  29. def OAI.MUB6.Certificate.PairSemantics.raw4102step2 line 146
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4102 line 148
  31. def OAI.MUB6.Certificate.PairSemantics.raw4103 line 166
  32. def OAI.MUB6.Certificate.PairSemantics.raw4103step0 line 168
  33. def OAI.MUB6.Certificate.PairSemantics.raw4103step1 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw4103step2 line 172
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4103 line 174
  36. def OAI.MUB6.Certificate.PairSemantics.raw4104 line 192
  37. def OAI.MUB6.Certificate.PairSemantics.raw4104step0 line 194
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4104 line 196
  39. def OAI.MUB6.Certificate.PairSemantics.raw4105 line 205
  40. def OAI.MUB6.Certificate.PairSemantics.raw4105step0 line 207
  41. def OAI.MUB6.Certificate.PairSemantics.raw4105step1 line 209
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4105 line 211
  43. def OAI.MUB6.Certificate.PairSemantics.raw4106 line 224
  44. def OAI.MUB6.Certificate.PairSemantics.raw4106step0 line 226
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4106 line 228
  46. def OAI.MUB6.Certificate.PairSemantics.raw4107 line 237
  47. def OAI.MUB6.Certificate.PairSemantics.raw4107step0 line 239
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4107 line 241
  49. def OAI.MUB6.Certificate.PairSemantics.raw4108 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw4108step0 line 253
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4108 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw4109 line 265
  53. def OAI.MUB6.Certificate.PairSemantics.raw4109step0 line 267
  54. def OAI.MUB6.Certificate.PairSemantics.raw4109step1 line 269
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4109 line 271
  56. def OAI.MUB6.Certificate.PairSemantics.raw4110 line 285
  57. def OAI.MUB6.Certificate.PairSemantics.raw4110step0 line 287
  58. def OAI.MUB6.Certificate.PairSemantics.raw4110step1 line 289
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4110 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw4111 line 305
  61. def OAI.MUB6.Certificate.PairSemantics.raw4111step0 line 307
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4111 line 309
  63. def OAI.MUB6.Certificate.PairSemantics.raw4112 line 318
  64. def OAI.MUB6.Certificate.PairSemantics.raw4112step0 line 320
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4112 line 322
  66. def OAI.MUB6.Certificate.PairSemantics.raw4113 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw4113step0 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw4113step1 line 336
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4113 line 338
  70. def OAI.MUB6.Certificate.PairSemantics.raw4114 line 351
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4114 line 353
  72. def OAI.MUB6.Certificate.PairSemantics.raw4115 line 357
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4115 line 359
  74. def OAI.MUB6.Certificate.PairSemantics.raw4116 line 363
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4116 line 365
  76. def OAI.MUB6.Certificate.PairSemantics.raw4117 line 369
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4117 line 371
  78. def OAI.MUB6.Certificate.PairSemantics.raw4118 line 375
  79. def OAI.MUB6.Certificate.PairSemantics.raw4118step0 line 377
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4118 line 379
  81. def OAI.MUB6.Certificate.PairSemantics.raw4119 line 388
  82. def OAI.MUB6.Certificate.PairSemantics.raw4119step0 line 390
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4119 line 392
  84. def OAI.MUB6.Certificate.PairSemantics.raw4120 line 401
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4120 line 403
  86. def OAI.MUB6.Certificate.PairSemantics.raw4121 line 407
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4121 line 409
  88. def OAI.MUB6.Certificate.PairSemantics.raw4122 line 413
  89. def OAI.MUB6.Certificate.PairSemantics.raw4122step0 line 415
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4122 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw4123 line 426
  92. def OAI.MUB6.Certificate.PairSemantics.raw4123step0 line 428
  93. def OAI.MUB6.Certificate.PairSemantics.raw4123step1 line 430
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4123 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw4124 line 445
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4124 line 447
  97. def OAI.MUB6.Certificate.PairSemantics.raw4125 line 451
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical4125 line 453
  99. def OAI.MUB6.Certificate.PairSemantics.raw4126 line 457
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4126 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw4127 line 463
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4127 line 465