OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical152.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4864 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw4864step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw4864step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4864 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw4865 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw4865step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw4865step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4865 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw4866 line 56
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4866 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw4867 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw4867step0 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4867 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw4868 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw4868step0 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4868 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw4869 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw4869step0 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw4869step1 line 92
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4869 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw4870 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw4870step0 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw4870step1 line 111
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4870 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw4871 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw4871step0 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4871 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw4872 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw4872step0 line 141
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4872 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw4873 line 152
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4873 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw4874 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw4874step0 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw4874step1 line 162
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4874 line 164
  37. def OAI.MUB6.Certificate.PairSemantics.raw4875 line 177
  38. def OAI.MUB6.Certificate.PairSemantics.raw4875step0 line 179
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4875 line 181
  40. def OAI.MUB6.Certificate.PairSemantics.raw4876 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw4876step0 line 192
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4876 line 194
  43. def OAI.MUB6.Certificate.PairSemantics.raw4877 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw4877step0 line 205
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4877 line 207
  46. def OAI.MUB6.Certificate.PairSemantics.raw4878 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw4878step0 line 218
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4878 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw4879 line 229
  50. def OAI.MUB6.Certificate.PairSemantics.raw4879step0 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw4879step1 line 233
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4879 line 235
  53. def OAI.MUB6.Certificate.PairSemantics.raw4880 line 248
  54. def OAI.MUB6.Certificate.PairSemantics.raw4880step0 line 250
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4880 line 252
  56. def OAI.MUB6.Certificate.PairSemantics.raw4881 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw4881step0 line 263
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4881 line 265
  59. def OAI.MUB6.Certificate.PairSemantics.raw4882 line 274
  60. def OAI.MUB6.Certificate.PairSemantics.raw4882step0 line 276
  61. def OAI.MUB6.Certificate.PairSemantics.raw4882step1 line 278
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4882 line 280
  63. def OAI.MUB6.Certificate.PairSemantics.raw4883 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw4883step0 line 295
  65. def OAI.MUB6.Certificate.PairSemantics.raw4883step1 line 297
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4883 line 299
  67. def OAI.MUB6.Certificate.PairSemantics.raw4884 line 313
  68. def OAI.MUB6.Certificate.PairSemantics.raw4884step0 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw4884step1 line 317
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4884 line 319
  71. def OAI.MUB6.Certificate.PairSemantics.raw4885 line 332
  72. def OAI.MUB6.Certificate.PairSemantics.raw4885step0 line 334
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4885 line 336
  74. def OAI.MUB6.Certificate.PairSemantics.raw4886 line 345
  75. def OAI.MUB6.Certificate.PairSemantics.raw4886step0 line 347
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4886 line 349
  77. def OAI.MUB6.Certificate.PairSemantics.raw4887 line 358
  78. def OAI.MUB6.Certificate.PairSemantics.raw4887step0 line 360
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4887 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw4888 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw4888step0 line 373
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4888 line 375
  83. def OAI.MUB6.Certificate.PairSemantics.raw4889 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw4889step0 line 386
  85. def OAI.MUB6.Certificate.PairSemantics.raw4889step1 line 388
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4889 line 390
  87. def OAI.MUB6.Certificate.PairSemantics.raw4890 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw4890step0 line 405
  89. def OAI.MUB6.Certificate.PairSemantics.raw4890step1 line 407
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4890 line 409
  91. def OAI.MUB6.Certificate.PairSemantics.raw4891 line 422
  92. def OAI.MUB6.Certificate.PairSemantics.raw4891step0 line 424
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4891 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw4892 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw4892step0 line 437
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4892 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw4893 line 448
  98. def OAI.MUB6.Certificate.PairSemantics.raw4893step0 line 450
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical4893 line 452
  100. def OAI.MUB6.Certificate.PairSemantics.raw4894 line 461
  101. def OAI.MUB6.Certificate.PairSemantics.raw4894step0 line 463
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4894 line 465
  103. def OAI.MUB6.Certificate.PairSemantics.raw4895 line 474
  104. def OAI.MUB6.Certificate.PairSemantics.raw4895step0 line 476
  105. def OAI.MUB6.Certificate.PairSemantics.raw4895step1 line 478
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4895 line 480