OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons65.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4164 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4164 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4165 line 33
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4165 line 35
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4166 line 56
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4166 line 58
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4167 line 79
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4167 line 81
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4168 line 102
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4168 line 104
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4171 line 125
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4171 line 127
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4172 line 148
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4172 line 150
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4174 line 171
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4174 line 173
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4175 line 194
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4175 line 196
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4177 line 217
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4177 line 219
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4180 line 240
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4180 line 242
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4181 line 263
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4181 line 265
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4182 line 286
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4182 line 288
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4183 line 309
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4183 line 311
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4185 line 332
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4185 line 334
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4186 line 355
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4186 line 357
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4187 line 378
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4187 line 380
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4190 line 401
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4190 line 403
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4191 line 424
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4191 line 426
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4192 line 447
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4192 line 449
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4194 line 470
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4194 line 472
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4195 line 493
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4195 line 495
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4196 line 516
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4196 line 518
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4197 line 539
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4197 line 541
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4198 line 562
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4198 line 564
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4199 line 585
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4199 line 587
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4200 line 608
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4200 line 610
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4201 line 631
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4201 line 633
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4202 line 654
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4202 line 656
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4203 line 677
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4203 line 679
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4204 line 700
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4204 line 702
  63. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4205 line 723
  64. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4205 line 725
  65. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4206 line 746
  66. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4206 line 748
  67. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4207 line 769
  68. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4207 line 771
  69. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4208 line 792
  70. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4208 line 794
  71. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4210 line 815
  72. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4210 line 817
  73. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4212 line 838
  74. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4212 line 840
  75. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4213 line 861
  76. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4213 line 863
  77. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4217 line 884
  78. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4217 line 886
  79. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4219 line 907
  80. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4219 line 909
  81. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4220 line 930
  82. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4220 line 932
  83. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4223 line 953
  84. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4223 line 955