OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons79.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5056 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5056 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5059 line 32
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5059 line 34
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5070 line 55
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5070 line 57
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5072 line 78
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5072 line 80
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5073 line 101
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5073 line 103
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5075 line 124
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5075 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5076 line 147
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5076 line 149
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5078 line 170
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5078 line 172
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5080 line 193
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5080 line 195
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5081 line 216
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5081 line 218
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5093 line 239
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5093 line 241
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5094 line 262
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5094 line 264
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5095 line 285
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5095 line 287
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5098 line 308
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5098 line 310
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5099 line 331
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5099 line 333
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5102 line 354
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5102 line 356
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5105 line 377
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5105 line 379
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5109 line 400
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5109 line 402
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5110 line 423
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5110 line 425
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5114 line 446
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5114 line 448
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5117 line 469
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5117 line 471
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5118 line 492
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5118 line 494
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5119 line 515
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5119 line 517