OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons62.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3969 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3969 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3970 line 28
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3970 line 30
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3977 line 46
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3977 line 48
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3980 line 64
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3980 line 66
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3981 line 82
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3981 line 84
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3982 line 100
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3982 line 102
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3984 line 118
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3984 line 120
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3987 line 136
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3987 line 138
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3990 line 154
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3990 line 156
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3992 line 172
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3992 line 174
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3993 line 190
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3993 line 192
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3994 line 208
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3994 line 210
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3995 line 226
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3995 line 228
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3997 line 244
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3997 line 246
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3998 line 262
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3998 line 264
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4002 line 280
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4002 line 282
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4003 line 298
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4003 line 300
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4004 line 316
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4004 line 318
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4012 line 334
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4012 line 336
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4013 line 352
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4013 line 354
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4014 line 370
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4014 line 372
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4015 line 388
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4015 line 390
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4017 line 406
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4017 line 408
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4020 line 424
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4020 line 426
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4023 line 442
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4023 line 444
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4026 line 460
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4026 line 462
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4027 line 478
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4027 line 480
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4028 line 496
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4028 line 498
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4029 line 514
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4029 line 516
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4030 line 532
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4030 line 534
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4031 line 550
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4031 line 552