OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons70.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4489 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4489 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4490 line 32
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4490 line 34
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4491 line 55
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4491 line 57
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4493 line 78
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4493 line 80
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4495 line 101
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4495 line 103
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4496 line 124
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4496 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4499 line 147
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4499 line 149
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4503 line 170
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4503 line 172
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4507 line 193
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4507 line 195
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4510 line 216
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4510 line 218
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4513 line 239
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4513 line 241
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4514 line 262
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4514 line 264
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4515 line 285
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4515 line 287
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4516 line 308
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4516 line 310
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4517 line 331
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4517 line 333
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4518 line 354
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4518 line 356
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4519 line 377
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4519 line 379
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4520 line 400
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4520 line 402
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4521 line 423
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4521 line 425
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4522 line 446
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4522 line 448
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4523 line 469
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4523 line 471
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4524 line 492
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4524 line 494
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4525 line 515
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4525 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4526 line 538
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4526 line 540
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4537 line 561
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4537 line 563
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4538 line 584
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4538 line 586
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4539 line 607
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4539 line 609
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4541 line 630
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4541 line 632
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4543 line 653
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4543 line 655