OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical21.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw672 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw672step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw672step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical672 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw673 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw673step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw673step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical673 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw674 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw674step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw674step1 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical674 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw675 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw675step0 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw675step1 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical675 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw676 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw676step0 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw676step1 line 96
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical676 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw677 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw677step0 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw677step1 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical677 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw678 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw678step0 line 132
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical678 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw679 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw679step0 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw679step1 line 147
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical679 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw680 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw680step0 line 164
  34. def OAI.MUB6.Certificate.PairSemantics.raw680step1 line 166
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical680 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw681 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw681step0 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw681step1 line 185
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical681 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw682 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw682step0 line 202
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical682 line 204
  43. def OAI.MUB6.Certificate.PairSemantics.raw683 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw683step0 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw683step1 line 217
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical683 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw684 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw684step0 line 234
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical684 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw685 line 245
  51. def OAI.MUB6.Certificate.PairSemantics.raw685step0 line 247
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical685 line 249
  53. def OAI.MUB6.Certificate.PairSemantics.raw686 line 258
  54. def OAI.MUB6.Certificate.PairSemantics.raw686step0 line 260
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical686 line 262
  56. def OAI.MUB6.Certificate.PairSemantics.raw687 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw687step0 line 273
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical687 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw688 line 284
  60. def OAI.MUB6.Certificate.PairSemantics.raw688step0 line 286
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical688 line 288
  62. def OAI.MUB6.Certificate.PairSemantics.raw689 line 297
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical689 line 299
  64. def OAI.MUB6.Certificate.PairSemantics.raw690 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw690step0 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw690step1 line 307
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical690 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw691 line 323
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical691 line 325
  70. def OAI.MUB6.Certificate.PairSemantics.raw692 line 329
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical692 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw693 line 335
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical693 line 337
  74. def OAI.MUB6.Certificate.PairSemantics.raw694 line 341
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical694 line 343
  76. def OAI.MUB6.Certificate.PairSemantics.raw695 line 347
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical695 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw696 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw696step0 line 355
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical696 line 357
  81. def OAI.MUB6.Certificate.PairSemantics.raw697 line 366
  82. def OAI.MUB6.Certificate.PairSemantics.raw697step0 line 368
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical697 line 370
  84. def OAI.MUB6.Certificate.PairSemantics.raw698 line 379
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical698 line 381
  86. def OAI.MUB6.Certificate.PairSemantics.raw699 line 385
  87. def OAI.MUB6.Certificate.PairSemantics.raw699step0 line 387
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical699 line 389
  89. def OAI.MUB6.Certificate.PairSemantics.raw700 line 398
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical700 line 400
  91. def OAI.MUB6.Certificate.PairSemantics.raw701 line 404
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical701 line 406
  93. def OAI.MUB6.Certificate.PairSemantics.raw702 line 410
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical702 line 412
  95. def OAI.MUB6.Certificate.PairSemantics.raw703 line 416
  96. def OAI.MUB6.Certificate.PairSemantics.raw703step0 line 418
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical703 line 420