OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical147.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4704 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw4704step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4704 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw4705 line 31
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4705 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw4706 line 37
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4706 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw4707 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4707 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw4708 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw4708step0 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw4708step1 line 53
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4708 line 55
  14. def OAI.MUB6.Certificate.PairSemantics.raw4709 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4709 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw4710 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw4710step0 line 76
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4710 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw4711 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw4711step0 line 89
  21. def OAI.MUB6.Certificate.PairSemantics.raw4711step1 line 91
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4711 line 93
  23. def OAI.MUB6.Certificate.PairSemantics.raw4712 line 106
  24. def OAI.MUB6.Certificate.PairSemantics.raw4712step0 line 108
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4712 line 110
  26. def OAI.MUB6.Certificate.PairSemantics.raw4713 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw4713step0 line 121
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4713 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw4714 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw4714step0 line 134
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4714 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw4715 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw4715step0 line 147
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4715 line 149
  35. def OAI.MUB6.Certificate.PairSemantics.raw4716 line 158
  36. def OAI.MUB6.Certificate.PairSemantics.raw4716step0 line 160
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4716 line 162
  38. def OAI.MUB6.Certificate.PairSemantics.raw4717 line 171
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4717 line 173
  40. def OAI.MUB6.Certificate.PairSemantics.raw4718 line 177
  41. def OAI.MUB6.Certificate.PairSemantics.raw4718step0 line 179
  42. def OAI.MUB6.Certificate.PairSemantics.raw4718step1 line 181
  43. def OAI.MUB6.Certificate.PairSemantics.raw4718step2 line 183
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4718 line 185
  45. def OAI.MUB6.Certificate.PairSemantics.raw4719 line 202
  46. def OAI.MUB6.Certificate.PairSemantics.raw4719step0 line 204
  47. def OAI.MUB6.Certificate.PairSemantics.raw4719step1 line 206
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4719 line 208
  49. def OAI.MUB6.Certificate.PairSemantics.raw4720 line 221
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4720 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw4721 line 227
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4721 line 229
  53. def OAI.MUB6.Certificate.PairSemantics.raw4722 line 233
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4722 line 235
  55. def OAI.MUB6.Certificate.PairSemantics.raw4723 line 239
  56. def OAI.MUB6.Certificate.PairSemantics.raw4723step0 line 241
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4723 line 243
  58. def OAI.MUB6.Certificate.PairSemantics.raw4724 line 252
  59. def OAI.MUB6.Certificate.PairSemantics.raw4724step0 line 254
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4724 line 256
  61. def OAI.MUB6.Certificate.PairSemantics.raw4725 line 265
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4725 line 267
  63. def OAI.MUB6.Certificate.PairSemantics.raw4726 line 271
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4726 line 273
  65. def OAI.MUB6.Certificate.PairSemantics.raw4727 line 277
  66. def OAI.MUB6.Certificate.PairSemantics.raw4727step0 line 279
  67. def OAI.MUB6.Certificate.PairSemantics.raw4727step1 line 281
  68. def OAI.MUB6.Certificate.PairSemantics.raw4727step2 line 283
  69. def OAI.MUB6.Certificate.PairSemantics.raw4727step3 line 285
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4727 line 287
  71. def OAI.MUB6.Certificate.PairSemantics.raw4728 line 309
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4728 line 311
  73. def OAI.MUB6.Certificate.PairSemantics.raw4729 line 315
  74. def OAI.MUB6.Certificate.PairSemantics.raw4729step0 line 317
  75. def OAI.MUB6.Certificate.PairSemantics.raw4729step1 line 319
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical4729 line 321
  77. def OAI.MUB6.Certificate.PairSemantics.raw4730 line 334
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4730 line 336
  79. def OAI.MUB6.Certificate.PairSemantics.raw4731 line 340
  80. def OAI.MUB6.Certificate.PairSemantics.raw4731step0 line 342
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4731 line 344
  82. def OAI.MUB6.Certificate.PairSemantics.raw4732 line 353
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4732 line 355
  84. def OAI.MUB6.Certificate.PairSemantics.raw4733 line 359
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4733 line 361
  86. def OAI.MUB6.Certificate.PairSemantics.raw4734 line 365
  87. def OAI.MUB6.Certificate.PairSemantics.raw4734step0 line 367
  88. def OAI.MUB6.Certificate.PairSemantics.raw4734step1 line 369
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4734 line 371
  90. def OAI.MUB6.Certificate.PairSemantics.raw4735 line 384
  91. def OAI.MUB6.Certificate.PairSemantics.raw4735step0 line 386
  92. def OAI.MUB6.Certificate.PairSemantics.raw4735step1 line 388
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4735 line 390