OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical146.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4672 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4672step0 line 22
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4672 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw4673 line 33
  5. def OAI.MUB6.Certificate.PairSemantics.raw4673step0 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw4673step1 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw4673step2 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4673 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw4674 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw4674step0 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw4674step1 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4674 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw4675 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw4675step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw4675step1 line 81
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4675 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw4676 line 96
  18. def OAI.MUB6.Certificate.PairSemantics.raw4676step0 line 98
  19. def OAI.MUB6.Certificate.PairSemantics.raw4676step1 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw4676step2 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4676 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw4677 line 121
  23. def OAI.MUB6.Certificate.PairSemantics.raw4677step0 line 123
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4677 line 125
  25. def OAI.MUB6.Certificate.PairSemantics.raw4678 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw4678step0 line 136
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4678 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw4679 line 147
  29. def OAI.MUB6.Certificate.PairSemantics.raw4679step0 line 149
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4679 line 151
  31. def OAI.MUB6.Certificate.PairSemantics.raw4680 line 160
  32. def OAI.MUB6.Certificate.PairSemantics.raw4680step0 line 162
  33. def OAI.MUB6.Certificate.PairSemantics.raw4680step1 line 164
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4680 line 166
  35. def OAI.MUB6.Certificate.PairSemantics.raw4681 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw4681step0 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw4681step1 line 183
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical4681 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw4682 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw4682step0 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw4682step1 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw4682step2 line 204
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4682 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw4683 line 223
  45. def OAI.MUB6.Certificate.PairSemantics.raw4683step0 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw4683step1 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw4683step2 line 229
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4683 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw4684 line 248
  50. def OAI.MUB6.Certificate.PairSemantics.raw4684step0 line 250
  51. def OAI.MUB6.Certificate.PairSemantics.raw4684step1 line 252
  52. def OAI.MUB6.Certificate.PairSemantics.raw4684step2 line 254
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4684 line 256
  54. def OAI.MUB6.Certificate.PairSemantics.raw4685 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw4685step0 line 275
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4685 line 277
  57. def OAI.MUB6.Certificate.PairSemantics.raw4686 line 286
  58. def OAI.MUB6.Certificate.PairSemantics.raw4686step0 line 288
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4686 line 290
  60. def OAI.MUB6.Certificate.PairSemantics.raw4687 line 299
  61. def OAI.MUB6.Certificate.PairSemantics.raw4687step0 line 301
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4687 line 303
  63. def OAI.MUB6.Certificate.PairSemantics.raw4688 line 312
  64. def OAI.MUB6.Certificate.PairSemantics.raw4688step0 line 314
  65. def OAI.MUB6.Certificate.PairSemantics.raw4688step1 line 316
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4688 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw4689 line 331
  68. def OAI.MUB6.Certificate.PairSemantics.raw4689step0 line 333
  69. def OAI.MUB6.Certificate.PairSemantics.raw4689step1 line 335
  70. def OAI.MUB6.Certificate.PairSemantics.raw4689step2 line 337
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4689 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw4690 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw4690step0 line 358
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4690 line 360
  75. def OAI.MUB6.Certificate.PairSemantics.raw4691 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw4691step0 line 371
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4691 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw4692 line 382
  79. def OAI.MUB6.Certificate.PairSemantics.raw4692step0 line 384
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4692 line 386
  81. def OAI.MUB6.Certificate.PairSemantics.raw4693 line 395
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4693 line 397
  83. def OAI.MUB6.Certificate.PairSemantics.raw4694 line 401
  84. def OAI.MUB6.Certificate.PairSemantics.raw4694step0 line 403
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4694 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw4695 line 414
  87. def OAI.MUB6.Certificate.PairSemantics.raw4695step0 line 416
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4695 line 418
  89. def OAI.MUB6.Certificate.PairSemantics.raw4696 line 427
  90. def OAI.MUB6.Certificate.PairSemantics.raw4696step0 line 429
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4696 line 431
  92. def OAI.MUB6.Certificate.PairSemantics.raw4697 line 440
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4697 line 442
  94. def OAI.MUB6.Certificate.PairSemantics.raw4698 line 446
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical4698 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw4699 line 452
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4699 line 454
  98. def OAI.MUB6.Certificate.PairSemantics.raw4700 line 458
  99. def OAI.MUB6.Certificate.PairSemantics.raw4700step0 line 460
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical4700 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw4701 line 471
  102. def OAI.MUB6.Certificate.PairSemantics.raw4701step0 line 473
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4701 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw4702 line 484
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical4702 line 486
  106. def OAI.MUB6.Certificate.PairSemantics.raw4703 line 490
  107. def OAI.MUB6.Certificate.PairSemantics.raw4703step0 line 492
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4703 line 494