OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical155.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4960 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw4960step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4960 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw4961 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw4961step0 line 32
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical4961 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw4962 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw4962step0 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4962 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw4963 line 56
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4963 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw4964 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw4964step0 line 64
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4964 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw4965 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4965 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw4966 line 81
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4966 line 83
  19. def OAI.MUB6.Certificate.PairSemantics.raw4967 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw4967step0 line 89
  21. def OAI.MUB6.Certificate.PairSemantics.raw4967step1 line 91
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4967 line 93
  23. def OAI.MUB6.Certificate.PairSemantics.raw4968 line 106
  24. def OAI.MUB6.Certificate.PairSemantics.raw4968step0 line 108
  25. def OAI.MUB6.Certificate.PairSemantics.raw4968step1 line 110
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4968 line 112
  27. def OAI.MUB6.Certificate.PairSemantics.raw4969 line 125
  28. def OAI.MUB6.Certificate.PairSemantics.raw4969step0 line 127
  29. def OAI.MUB6.Certificate.PairSemantics.raw4969step1 line 129
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4969 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw4970 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw4970step0 line 146
  33. def OAI.MUB6.Certificate.PairSemantics.raw4970step1 line 148
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4970 line 150
  35. def OAI.MUB6.Certificate.PairSemantics.raw4971 line 163
  36. def OAI.MUB6.Certificate.PairSemantics.raw4971step0 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw4971step1 line 167
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4971 line 169
  39. def OAI.MUB6.Certificate.PairSemantics.raw4972 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw4972step0 line 184
  41. def OAI.MUB6.Certificate.PairSemantics.raw4972step1 line 186
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4972 line 188
  43. def OAI.MUB6.Certificate.PairSemantics.raw4973 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw4973step0 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw4973step1 line 205
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4973 line 207
  47. def OAI.MUB6.Certificate.PairSemantics.raw4974 line 220
  48. def OAI.MUB6.Certificate.PairSemantics.raw4974step0 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw4974step1 line 224
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4974 line 226
  51. def OAI.MUB6.Certificate.PairSemantics.raw4975 line 239
  52. def OAI.MUB6.Certificate.PairSemantics.raw4975step0 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw4975step1 line 243
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4975 line 245
  55. def OAI.MUB6.Certificate.PairSemantics.raw4976 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw4976step0 line 260
  57. def OAI.MUB6.Certificate.PairSemantics.raw4976step1 line 262
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4976 line 264
  59. def OAI.MUB6.Certificate.PairSemantics.raw4977 line 277
  60. def OAI.MUB6.Certificate.PairSemantics.raw4977step0 line 279
  61. def OAI.MUB6.Certificate.PairSemantics.raw4977step1 line 281
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4977 line 283
  63. def OAI.MUB6.Certificate.PairSemantics.raw4978 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw4978step0 line 298
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4978 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw4979 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw4979step0 line 311
  68. def OAI.MUB6.Certificate.PairSemantics.raw4979step1 line 313
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4979 line 315
  70. def OAI.MUB6.Certificate.PairSemantics.raw4980 line 328
  71. def OAI.MUB6.Certificate.PairSemantics.raw4980step0 line 330
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4980 line 332
  73. def OAI.MUB6.Certificate.PairSemantics.raw4981 line 341
  74. def OAI.MUB6.Certificate.PairSemantics.raw4981step0 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw4981step1 line 345
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4981 line 347
  77. def OAI.MUB6.Certificate.PairSemantics.raw4982 line 360
  78. def OAI.MUB6.Certificate.PairSemantics.raw4982step0 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw4982step1 line 364
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4982 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw4983 line 379
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4983 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw4984 line 385
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4984 line 387
  85. def OAI.MUB6.Certificate.PairSemantics.raw4985 line 391
  86. def OAI.MUB6.Certificate.PairSemantics.raw4985step0 line 393
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4985 line 395
  88. def OAI.MUB6.Certificate.PairSemantics.raw4986 line 404
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4986 line 406
  90. def OAI.MUB6.Certificate.PairSemantics.raw4987 line 410
  91. def OAI.MUB6.Certificate.PairSemantics.raw4987step0 line 412
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical4987 line 414
  93. def OAI.MUB6.Certificate.PairSemantics.raw4988 line 423
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4988 line 425
  95. def OAI.MUB6.Certificate.PairSemantics.raw4989 line 429
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4989 line 431
  97. def OAI.MUB6.Certificate.PairSemantics.raw4990 line 435
  98. def OAI.MUB6.Certificate.PairSemantics.raw4990step0 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw4990step1 line 439
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4990 line 441
  101. def OAI.MUB6.Certificate.PairSemantics.raw4991 line 454
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4991 line 456