OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical120.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3840 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw3840step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw3840step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3840 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw3841 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw3841step0 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3841 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw3842 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw3842step0 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw3842step1 line 53
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3842 line 55
  12. def OAI.MUB6.Certificate.PairSemantics.raw3843 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw3843step0 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3843 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw3844 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw3844step0 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw3844step1 line 85
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3844 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw3845 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw3845step0 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3845 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw3846 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw3846step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw3846step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3846 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw3847 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw3847step0 line 134
  28. def OAI.MUB6.Certificate.PairSemantics.raw3847step1 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw3847step2 line 138
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3847 line 140
  31. def OAI.MUB6.Certificate.PairSemantics.raw3848 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw3848step0 line 159
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3848 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw3849 line 170
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3849 line 172
  36. def OAI.MUB6.Certificate.PairSemantics.raw3850 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw3850step0 line 178
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3850 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw3851 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw3851step0 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3851 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw3852 line 202
  43. def OAI.MUB6.Certificate.PairSemantics.raw3852step0 line 204
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical3852 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw3853 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw3853step0 line 217
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3853 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw3854 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw3854step0 line 230
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3854 line 232
  51. def OAI.MUB6.Certificate.PairSemantics.raw3855 line 241
  52. def OAI.MUB6.Certificate.PairSemantics.raw3855step0 line 243
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3855 line 245
  54. def OAI.MUB6.Certificate.PairSemantics.raw3856 line 254
  55. def OAI.MUB6.Certificate.PairSemantics.raw3856step0 line 256
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3856 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw3857 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw3857step0 line 269
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3857 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw3858 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw3858step0 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw3858step1 line 284
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3858 line 286
  64. def OAI.MUB6.Certificate.PairSemantics.raw3859 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw3859step0 line 301
  66. def OAI.MUB6.Certificate.PairSemantics.raw3859step1 line 303
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical3859 line 305
  68. def OAI.MUB6.Certificate.PairSemantics.raw3860 line 318
  69. def OAI.MUB6.Certificate.PairSemantics.raw3860step0 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw3860step1 line 322
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3860 line 324
  72. def OAI.MUB6.Certificate.PairSemantics.raw3861 line 337
  73. def OAI.MUB6.Certificate.PairSemantics.raw3861step0 line 339
  74. def OAI.MUB6.Certificate.PairSemantics.raw3861step1 line 341
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3861 line 343
  76. def OAI.MUB6.Certificate.PairSemantics.raw3862 line 356
  77. def OAI.MUB6.Certificate.PairSemantics.raw3862step0 line 358
  78. def OAI.MUB6.Certificate.PairSemantics.raw3862step1 line 360
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3862 line 362
  80. def OAI.MUB6.Certificate.PairSemantics.raw3863 line 375
  81. def OAI.MUB6.Certificate.PairSemantics.raw3863step0 line 377
  82. def OAI.MUB6.Certificate.PairSemantics.raw3863step1 line 379
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical3863 line 381
  84. def OAI.MUB6.Certificate.PairSemantics.raw3864 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw3864step0 line 396
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3864 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw3865 line 407
  88. def OAI.MUB6.Certificate.PairSemantics.raw3865step0 line 409
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3865 line 411
  90. def OAI.MUB6.Certificate.PairSemantics.raw3866 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw3866step0 line 422
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3866 line 424
  93. def OAI.MUB6.Certificate.PairSemantics.raw3867 line 433
  94. def OAI.MUB6.Certificate.PairSemantics.raw3867step0 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw3867step1 line 437
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3867 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw3868 line 452
  98. def OAI.MUB6.Certificate.PairSemantics.raw3868step0 line 454
  99. def OAI.MUB6.Certificate.PairSemantics.raw3868step1 line 456
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3868 line 458
  101. def OAI.MUB6.Certificate.PairSemantics.raw3869 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw3869step0 line 473
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical3869 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw3870 line 484
  105. def OAI.MUB6.Certificate.PairSemantics.raw3870step0 line 486
  106. def OAI.MUB6.Certificate.PairSemantics.raw3870step1 line 488
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3870 line 490
  108. def OAI.MUB6.Certificate.PairSemantics.raw3871 line 503
  109. def OAI.MUB6.Certificate.PairSemantics.raw3871step0 line 505
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3871 line 507