OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons64.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4096 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4096 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4098 line 28
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4098 line 30
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4099 line 51
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4099 line 53
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4100 line 74
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4100 line 76
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4101 line 97
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4101 line 99
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4102 line 120
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4102 line 122
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4103 line 143
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4103 line 145
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4104 line 166
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4104 line 168
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4105 line 189
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4105 line 191
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4106 line 212
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4106 line 214
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4107 line 235
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4107 line 237
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4108 line 258
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4108 line 260
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4109 line 281
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4109 line 283
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4110 line 304
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4110 line 306
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4111 line 327
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4111 line 329
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4112 line 350
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4112 line 352
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4113 line 373
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4113 line 375
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4114 line 396
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4114 line 398
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4115 line 419
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4115 line 421
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4116 line 442
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4116 line 444
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4119 line 465
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4119 line 467
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4121 line 488
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4121 line 490
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4122 line 511
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4122 line 513
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4126 line 534
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4126 line 536
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4128 line 557
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4128 line 559
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4129 line 580
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4129 line 582
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4132 line 603
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4132 line 605
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4133 line 626
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4133 line 628
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4134 line 649
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4134 line 651
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4135 line 672
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4135 line 674
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4138 line 695
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4138 line 697
  63. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4139 line 718
  64. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4139 line 720
  65. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4140 line 741
  66. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4140 line 743
  67. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4141 line 764
  68. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4141 line 766
  69. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4142 line 787
  70. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4142 line 789
  71. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4143 line 810
  72. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4143 line 812
  73. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4144 line 833
  74. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4144 line 835
  75. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4145 line 856
  76. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4145 line 858
  77. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4146 line 879
  78. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4146 line 881
  79. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4147 line 902
  80. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4147 line 904
  81. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4148 line 925
  82. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4148 line 927