OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources86.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA2752 line 13
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB2752 line 14
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC2752 line 15
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2752 line 16
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2752 line 18
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA2753 line 69
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB2753 line 70
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC2753 line 71
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2753 line 72
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2753 line 74
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA2754 line 125
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB2754 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC2754 line 127
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2754 line 128
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2754 line 130
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA2755 line 181
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB2755 line 182
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC2755 line 183
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2755 line 184
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2755 line 186
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA2756 line 237
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB2756 line 238
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC2756 line 239
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2756 line 240
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2756 line 242
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA2757 line 293
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB2757 line 294
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC2757 line 295
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2757 line 296
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2757 line 298
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA2758 line 349
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB2758 line 350
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC2758 line 351
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2758 line 352
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2758 line 354
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA2759 line 405
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB2759 line 406
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC2759 line 407
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2759 line 408
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2759 line 410
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA2760 line 461
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB2760 line 462
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC2760 line 463
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2760 line 464
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2760 line 466
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA2761 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB2761 line 518
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC2761 line 519
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2761 line 520
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2761 line 522
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA2762 line 573
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB2762 line 574
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC2762 line 575
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2762 line 576
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2762 line 578
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA2763 line 629
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB2763 line 630
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC2763 line 631
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2763 line 632
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2763 line 634
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA2764 line 685
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB2764 line 686
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC2764 line 687
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2764 line 688
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2764 line 690
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA2765 line 741
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB2765 line 742
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC2765 line 743
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2765 line 744
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2765 line 746
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA2766 line 797
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB2766 line 798
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC2766 line 799
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm2766 line 800
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq2766 line 802