OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons73.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4672 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4672 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4673 line 32
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4673 line 34
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4674 line 55
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4674 line 57
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4676 line 78
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4676 line 80
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4678 line 101
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4678 line 103
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4679 line 124
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4679 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4681 line 147
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4681 line 149
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4684 line 170
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4684 line 172
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4685 line 193
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4685 line 195
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4686 line 216
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4686 line 218
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4688 line 239
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4688 line 241
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4689 line 262
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4689 line 264
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4691 line 285
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4691 line 287
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4692 line 308
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4692 line 310
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4693 line 331
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4693 line 333
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4706 line 354
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4706 line 356
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4707 line 377
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4707 line 379
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4709 line 400
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4709 line 402
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4710 line 423
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4710 line 425
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4713 line 446
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4713 line 448
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4714 line 469
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4714 line 471
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4716 line 492
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4716 line 494
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4717 line 515
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4717 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4719 line 538
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4719 line 540
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4720 line 561
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4720 line 563
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4721 line 584
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4721 line 586
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4722 line 607
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4722 line 609
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4723 line 630
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4723 line 632
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4724 line 653
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4724 line 655
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4725 line 676
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4725 line 678
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4726 line 699
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4726 line 701
  63. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4727 line 722
  64. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4727 line 724
  65. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4728 line 745
  66. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4728 line 747
  67. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4729 line 768
  68. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4729 line 770
  69. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4731 line 791
  70. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4731 line 793
  71. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4732 line 814
  72. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4732 line 816