OAI/Analysis/MutuallyUnbiased/TaoCertificate/Merge45.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.TaoCertificate.combined360_part0 line 8
  2. def OAI.MUB6.TaoCertificate.combined360_part1 line 10
  3. def OAI.MUB6.TaoCertificate.combined360_part2 line 12
  4. def OAI.MUB6.TaoCertificate.combined360 line 14
  5. theorem OAI.MUB6.TaoCertificate.combined360_checked line 16
  6. theorem OAI.MUB6.TaoCertificate.combined360_zero line 19
  7. def OAI.MUB6.TaoCertificate.combined361_part0 line 27
  8. def OAI.MUB6.TaoCertificate.combined361_part1 line 29
  9. def OAI.MUB6.TaoCertificate.combined361_part2 line 31
  10. def OAI.MUB6.TaoCertificate.combined361 line 33
  11. theorem OAI.MUB6.TaoCertificate.combined361_checked line 35
  12. theorem OAI.MUB6.TaoCertificate.combined361_zero line 38
  13. def OAI.MUB6.TaoCertificate.combined362_part0 line 46
  14. def OAI.MUB6.TaoCertificate.combined362_part1 line 48
  15. def OAI.MUB6.TaoCertificate.combined362_part2 line 50
  16. def OAI.MUB6.TaoCertificate.combined362_part3 line 52
  17. def OAI.MUB6.TaoCertificate.combined362 line 54
  18. theorem OAI.MUB6.TaoCertificate.combined362_checked line 56
  19. theorem OAI.MUB6.TaoCertificate.combined362_zero line 59
  20. def OAI.MUB6.TaoCertificate.combined363_part0 line 67
  21. def OAI.MUB6.TaoCertificate.combined363_part1 line 69
  22. def OAI.MUB6.TaoCertificate.combined363_part2 line 71
  23. def OAI.MUB6.TaoCertificate.combined363_part3 line 73
  24. def OAI.MUB6.TaoCertificate.combined363 line 75
  25. theorem OAI.MUB6.TaoCertificate.combined363_checked line 77
  26. theorem OAI.MUB6.TaoCertificate.combined363_zero line 80
  27. def OAI.MUB6.TaoCertificate.combined364_part0 line 88
  28. def OAI.MUB6.TaoCertificate.combined364_part1 line 90
  29. def OAI.MUB6.TaoCertificate.combined364_part2 line 92
  30. def OAI.MUB6.TaoCertificate.combined364_part3 line 94
  31. def OAI.MUB6.TaoCertificate.combined364_part4 line 96
  32. def OAI.MUB6.TaoCertificate.combined364 line 98
  33. theorem OAI.MUB6.TaoCertificate.combined364_checked line 100
  34. theorem OAI.MUB6.TaoCertificate.combined364_zero line 103
  35. def OAI.MUB6.TaoCertificate.combined365_part0 line 111
  36. def OAI.MUB6.TaoCertificate.combined365_part1 line 113
  37. def OAI.MUB6.TaoCertificate.combined365_part2 line 115
  38. def OAI.MUB6.TaoCertificate.combined365_part3 line 117
  39. def OAI.MUB6.TaoCertificate.combined365_part4 line 119
  40. def OAI.MUB6.TaoCertificate.combined365 line 121
  41. theorem OAI.MUB6.TaoCertificate.combined365_checked line 123
  42. theorem OAI.MUB6.TaoCertificate.combined365_zero line 126
  43. def OAI.MUB6.TaoCertificate.combined366_part0 line 134
  44. def OAI.MUB6.TaoCertificate.combined366_part1 line 136
  45. def OAI.MUB6.TaoCertificate.combined366_part2 line 138
  46. def OAI.MUB6.TaoCertificate.combined366_part3 line 140
  47. def OAI.MUB6.TaoCertificate.combined366_part4 line 142
  48. def OAI.MUB6.TaoCertificate.combined366_part5 line 144
  49. def OAI.MUB6.TaoCertificate.combined366 line 146
  50. theorem OAI.MUB6.TaoCertificate.combined366_checked line 148
  51. theorem OAI.MUB6.TaoCertificate.combined366_zero line 151
  52. def OAI.MUB6.TaoCertificate.combined367_part0 line 159
  53. def OAI.MUB6.TaoCertificate.combined367_part1 line 161
  54. def OAI.MUB6.TaoCertificate.combined367_part2 line 163
  55. def OAI.MUB6.TaoCertificate.combined367_part3 line 165
  56. def OAI.MUB6.TaoCertificate.combined367_part4 line 167
  57. def OAI.MUB6.TaoCertificate.combined367_part5 line 169
  58. def OAI.MUB6.TaoCertificate.combined367 line 171
  59. theorem OAI.MUB6.TaoCertificate.combined367_checked line 173
  60. theorem OAI.MUB6.TaoCertificate.combined367_zero line 176