OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical314.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10048 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw10048step0 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw10048step1 line 17
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical10048 line 19
  5. def OAI.MUB6.Certificate.PairSemantics.raw10049 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw10049step0 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical10049 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw10050 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw10050step0 line 47
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical10050 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw10051 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw10051step0 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical10051 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw10052 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw10052step0 line 73
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical10052 line 75
  17. def OAI.MUB6.Certificate.PairSemantics.raw10053 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw10053step0 line 86
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical10053 line 88
  20. def OAI.MUB6.Certificate.PairSemantics.raw10054 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw10054step0 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw10054step1 line 101
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical10054 line 103
  24. def OAI.MUB6.Certificate.PairSemantics.raw10055 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw10055step0 line 118
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical10055 line 120
  27. def OAI.MUB6.Certificate.PairSemantics.raw10056 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw10056step0 line 131
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical10056 line 133
  30. def OAI.MUB6.Certificate.PairSemantics.raw10057 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw10057step0 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw10057step1 line 146
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical10057 line 148
  34. def OAI.MUB6.Certificate.PairSemantics.raw10058 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw10058step0 line 163
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical10058 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw10059 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw10059step0 line 176
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical10059 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw10060 line 187
  41. def OAI.MUB6.Certificate.PairSemantics.raw10060step0 line 189
  42. def OAI.MUB6.Certificate.PairSemantics.raw10060step1 line 191
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical10060 line 193
  44. def OAI.MUB6.Certificate.PairSemantics.raw10061 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw10061step0 line 208
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical10061 line 210
  47. def OAI.MUB6.Certificate.PairSemantics.raw10062 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw10062step0 line 221
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical10062 line 223
  50. def OAI.MUB6.Certificate.PairSemantics.raw10063 line 232
  51. def OAI.MUB6.Certificate.PairSemantics.raw10063step0 line 234
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical10063 line 236
  53. def OAI.MUB6.Certificate.PairSemantics.raw10064 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw10064step0 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical10064 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw10065 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw10065step0 line 260
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical10065 line 262
  59. def OAI.MUB6.Certificate.PairSemantics.raw10066 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw10066step0 line 273
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical10066 line 275
  62. def OAI.MUB6.Certificate.PairSemantics.raw10067 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw10067step0 line 286
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical10067 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw10068 line 297
  66. def OAI.MUB6.Certificate.PairSemantics.raw10068step0 line 299
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical10068 line 301
  68. def OAI.MUB6.Certificate.PairSemantics.raw10069 line 310
  69. def OAI.MUB6.Certificate.PairSemantics.raw10069step0 line 312
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical10069 line 314
  71. def OAI.MUB6.Certificate.PairSemantics.raw10070 line 323
  72. def OAI.MUB6.Certificate.PairSemantics.raw10070step0 line 325
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical10070 line 327
  74. def OAI.MUB6.Certificate.PairSemantics.raw10071 line 336
  75. def OAI.MUB6.Certificate.PairSemantics.raw10071step0 line 338
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical10071 line 340
  77. def OAI.MUB6.Certificate.PairSemantics.raw10072 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw10072step0 line 351
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical10072 line 353
  80. def OAI.MUB6.Certificate.PairSemantics.raw10073 line 362
  81. def OAI.MUB6.Certificate.PairSemantics.raw10073step0 line 364
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical10073 line 366
  83. def OAI.MUB6.Certificate.PairSemantics.raw10074 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw10074step0 line 377
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical10074 line 379
  86. def OAI.MUB6.Certificate.PairSemantics.raw10075 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw10075step0 line 390
  88. def OAI.MUB6.Certificate.PairSemantics.raw10075step1 line 392
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical10075 line 394
  90. def OAI.MUB6.Certificate.PairSemantics.raw10076 line 407
  91. def OAI.MUB6.Certificate.PairSemantics.raw10076step0 line 409
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical10076 line 411
  93. def OAI.MUB6.Certificate.PairSemantics.raw10077 line 420
  94. def OAI.MUB6.Certificate.PairSemantics.raw10077step0 line 422
  95. def OAI.MUB6.Certificate.PairSemantics.raw10077step1 line 424
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical10077 line 426
  97. def OAI.MUB6.Certificate.PairSemantics.raw10078 line 439
  98. def OAI.MUB6.Certificate.PairSemantics.raw10078step0 line 441
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical10078 line 443
  100. def OAI.MUB6.Certificate.PairSemantics.raw10079 line 452
  101. def OAI.MUB6.Certificate.PairSemantics.raw10079step0 line 454
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical10079 line 456