OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical154.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4928 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw4928step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw4928step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4928 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw4929 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical4929 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw4930 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4930 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw4931 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4931 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw4932 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4932 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw4933 line 58
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4933 line 60
  15. def OAI.MUB6.Certificate.PairSemantics.raw4934 line 64
  16. def OAI.MUB6.Certificate.PairSemantics.raw4934step0 line 66
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4934 line 68
  18. def OAI.MUB6.Certificate.PairSemantics.raw4935 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw4935step0 line 80
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4935 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw4936 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw4936step0 line 94
  23. def OAI.MUB6.Certificate.PairSemantics.raw4936step1 line 96
  24. def OAI.MUB6.Certificate.PairSemantics.raw4936step2 line 98
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4936 line 100
  26. def OAI.MUB6.Certificate.PairSemantics.raw4937 line 118
  27. def OAI.MUB6.Certificate.PairSemantics.raw4937step0 line 120
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4937 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw4938 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw4938step0 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw4938step1 line 136
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4938 line 138
  33. def OAI.MUB6.Certificate.PairSemantics.raw4939 line 151
  34. def OAI.MUB6.Certificate.PairSemantics.raw4939step0 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw4939step1 line 155
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4939 line 157
  37. def OAI.MUB6.Certificate.PairSemantics.raw4940 line 170
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4940 line 172
  39. def OAI.MUB6.Certificate.PairSemantics.raw4941 line 176
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4941 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw4942 line 182
  42. def OAI.MUB6.Certificate.PairSemantics.raw4942step0 line 184
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4942 line 186
  44. def OAI.MUB6.Certificate.PairSemantics.raw4943 line 195
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4943 line 197
  46. def OAI.MUB6.Certificate.PairSemantics.raw4944 line 201
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4944 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw4945 line 207
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical4945 line 209
  50. def OAI.MUB6.Certificate.PairSemantics.raw4946 line 213
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4946 line 215
  52. def OAI.MUB6.Certificate.PairSemantics.raw4947 line 219
  53. def OAI.MUB6.Certificate.PairSemantics.raw4947step0 line 221
  54. def OAI.MUB6.Certificate.PairSemantics.raw4947step1 line 223
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4947 line 225
  56. def OAI.MUB6.Certificate.PairSemantics.raw4948 line 238
  57. def OAI.MUB6.Certificate.PairSemantics.raw4948step0 line 240
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4948 line 242
  59. def OAI.MUB6.Certificate.PairSemantics.raw4949 line 252
  60. def OAI.MUB6.Certificate.PairSemantics.raw4949step0 line 254
  61. def OAI.MUB6.Certificate.PairSemantics.raw4949step1 line 256
  62. def OAI.MUB6.Certificate.PairSemantics.raw4949step2 line 258
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4949 line 260
  64. def OAI.MUB6.Certificate.PairSemantics.raw4950 line 278
  65. def OAI.MUB6.Certificate.PairSemantics.raw4950step0 line 280
  66. def OAI.MUB6.Certificate.PairSemantics.raw4950step1 line 282
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4950 line 284
  68. def OAI.MUB6.Certificate.PairSemantics.raw4951 line 298
  69. def OAI.MUB6.Certificate.PairSemantics.raw4951step0 line 300
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4951 line 302
  71. def OAI.MUB6.Certificate.PairSemantics.raw4952 line 311
  72. def OAI.MUB6.Certificate.PairSemantics.raw4952step0 line 313
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4952 line 315
  74. def OAI.MUB6.Certificate.PairSemantics.raw4953 line 324
  75. def OAI.MUB6.Certificate.PairSemantics.raw4953step0 line 326
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4953 line 328
  77. def OAI.MUB6.Certificate.PairSemantics.raw4954 line 337
  78. def OAI.MUB6.Certificate.PairSemantics.raw4954step0 line 339
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4954 line 341
  80. def OAI.MUB6.Certificate.PairSemantics.raw4955 line 350
  81. def OAI.MUB6.Certificate.PairSemantics.raw4955step0 line 352
  82. def OAI.MUB6.Certificate.PairSemantics.raw4955step1 line 354
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4955 line 356
  84. def OAI.MUB6.Certificate.PairSemantics.raw4956 line 369
  85. def OAI.MUB6.Certificate.PairSemantics.raw4956step0 line 371
  86. def OAI.MUB6.Certificate.PairSemantics.raw4956step1 line 373
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4956 line 375
  88. def OAI.MUB6.Certificate.PairSemantics.raw4957 line 388
  89. def OAI.MUB6.Certificate.PairSemantics.raw4957step0 line 390
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4957 line 392
  91. def OAI.MUB6.Certificate.PairSemantics.raw4958 line 401
  92. def OAI.MUB6.Certificate.PairSemantics.raw4958step0 line 403
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4958 line 405
  94. def OAI.MUB6.Certificate.PairSemantics.raw4959 line 414
  95. def OAI.MUB6.Certificate.PairSemantics.raw4959step0 line 416
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4959 line 418