OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical33.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1056 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw1056step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw1056step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1056 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw1057 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1057 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw1058 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw1058step0 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw1058step1 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1058 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw1059 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw1059step0 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw1059step1 line 63
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1059 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw1060 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw1060step0 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw1060step1 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1060 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw1061 line 97
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1061 line 99
  21. def OAI.MUB6.Certificate.PairSemantics.raw1062 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw1062step0 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw1062step1 line 107
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1062 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw1063 line 122
  26. def OAI.MUB6.Certificate.PairSemantics.raw1063step0 line 124
  27. def OAI.MUB6.Certificate.PairSemantics.raw1063step1 line 126
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1063 line 128
  29. def OAI.MUB6.Certificate.PairSemantics.raw1064 line 141
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1064 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw1065 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw1065step0 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw1065step1 line 151
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1065 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw1066 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw1066step0 line 168
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1066 line 170
  38. def OAI.MUB6.Certificate.PairSemantics.raw1067 line 179
  39. def OAI.MUB6.Certificate.PairSemantics.raw1067step0 line 181
  40. def OAI.MUB6.Certificate.PairSemantics.raw1067step1 line 183
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1067 line 185
  42. def OAI.MUB6.Certificate.PairSemantics.raw1068 line 198
  43. def OAI.MUB6.Certificate.PairSemantics.raw1068step0 line 200
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1068 line 202
  45. def OAI.MUB6.Certificate.PairSemantics.raw1069 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw1069step0 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw1069step1 line 215
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1069 line 217
  49. def OAI.MUB6.Certificate.PairSemantics.raw1070 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw1070step0 line 232
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1070 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw1071 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw1071step0 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw1071step1 line 247
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1071 line 249
  56. def OAI.MUB6.Certificate.PairSemantics.raw1072 line 262
  57. def OAI.MUB6.Certificate.PairSemantics.raw1072step0 line 264
  58. def OAI.MUB6.Certificate.PairSemantics.raw1072step1 line 266
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1072 line 268
  60. def OAI.MUB6.Certificate.PairSemantics.raw1073 line 281
  61. def OAI.MUB6.Certificate.PairSemantics.raw1073step0 line 283
  62. def OAI.MUB6.Certificate.PairSemantics.raw1073step1 line 285
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1073 line 287
  64. def OAI.MUB6.Certificate.PairSemantics.raw1074 line 300
  65. def OAI.MUB6.Certificate.PairSemantics.raw1074step0 line 302
  66. def OAI.MUB6.Certificate.PairSemantics.raw1074step1 line 304
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1074 line 306
  68. def OAI.MUB6.Certificate.PairSemantics.raw1075 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw1075step0 line 321
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1075 line 323
  71. def OAI.MUB6.Certificate.PairSemantics.raw1076 line 332
  72. def OAI.MUB6.Certificate.PairSemantics.raw1076step0 line 334
  73. def OAI.MUB6.Certificate.PairSemantics.raw1076step1 line 336
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1076 line 338
  75. def OAI.MUB6.Certificate.PairSemantics.raw1077 line 351
  76. def OAI.MUB6.Certificate.PairSemantics.raw1077step0 line 353
  77. def OAI.MUB6.Certificate.PairSemantics.raw1077step1 line 355
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1077 line 357
  79. def OAI.MUB6.Certificate.PairSemantics.raw1078 line 370
  80. def OAI.MUB6.Certificate.PairSemantics.raw1078step0 line 372
  81. def OAI.MUB6.Certificate.PairSemantics.raw1078step1 line 374
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1078 line 376
  83. def OAI.MUB6.Certificate.PairSemantics.raw1079 line 389
  84. def OAI.MUB6.Certificate.PairSemantics.raw1079step0 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw1079step1 line 393
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1079 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw1080 line 408
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1080 line 410
  89. def OAI.MUB6.Certificate.PairSemantics.raw1081 line 414
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1081 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw1082 line 420
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1082 line 422
  93. def OAI.MUB6.Certificate.PairSemantics.raw1083 line 426
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1083 line 428
  95. def OAI.MUB6.Certificate.PairSemantics.raw1084 line 432
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1084 line 434
  97. def OAI.MUB6.Certificate.PairSemantics.raw1085 line 438
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1085 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw1086 line 444
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical1086 line 446
  101. def OAI.MUB6.Certificate.PairSemantics.raw1087 line 450
  102. def OAI.MUB6.Certificate.PairSemantics.raw1087step0 line 452
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1087 line 454