OAI/Analysis/MutuallyUnbiased/GramAssembly/Block0Part0.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block0.node0 line 7
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node0_check line 9
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node0_eval line 12
  4. def OAI.MUB6.Certificate.GramAssembly.Block0.node1 line 17
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node1_check line 19
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node1_eval line 22
  7. def OAI.MUB6.Certificate.GramAssembly.Block0.node2 line 27
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node2_check line 29
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node2_eval line 32
  10. def OAI.MUB6.Certificate.GramAssembly.Block0.node3 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node3_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node3_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block0.node4 line 48
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node4_check line 50
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node4_eval line 53
  16. def OAI.MUB6.Certificate.GramAssembly.Block0.node5 line 58
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node5_check line 60
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node5_eval line 63
  19. def OAI.MUB6.Certificate.GramAssembly.Block0.node6 line 68
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node6_check line 70
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node6_eval line 73
  22. def OAI.MUB6.Certificate.GramAssembly.Block0.node7 line 79
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node7_check line 81
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node7_eval line 84
  25. def OAI.MUB6.Certificate.GramAssembly.Block0.node8 line 89
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node8_check line 91
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node8_eval line 94
  28. def OAI.MUB6.Certificate.GramAssembly.Block0.node9 line 99
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node9_check line 101
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node9_eval line 104
  31. def OAI.MUB6.Certificate.GramAssembly.Block0.node10 line 109
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node10_check line 111
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node10_eval line 114
  34. def OAI.MUB6.Certificate.GramAssembly.Block0.node11 line 120
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node11_check line 122
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node11_eval line 125
  37. def OAI.MUB6.Certificate.GramAssembly.Block0.node12 line 130
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node12_check line 132
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node12_eval line 135
  40. def OAI.MUB6.Certificate.GramAssembly.Block0.node13 line 140
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node13_check line 142
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node13_eval line 145
  43. def OAI.MUB6.Certificate.GramAssembly.Block0.node14 line 150
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node14_check line 152
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node14_eval line 155
  46. def OAI.MUB6.Certificate.GramAssembly.Block0.node15 line 161
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node15_check line 163
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node15_eval line 166
  49. def OAI.MUB6.Certificate.GramAssembly.Block0.node16 line 171
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node16_check line 173
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node16_eval line 176
  52. def OAI.MUB6.Certificate.GramAssembly.Block0.node17 line 181
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node17_check line 183
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node17_eval line 186
  55. def OAI.MUB6.Certificate.GramAssembly.Block0.node18 line 191
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node18_check line 193
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node18_eval line 196
  58. def OAI.MUB6.Certificate.GramAssembly.Block0.node19 line 202
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node19_check line 204
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node19_eval line 207
  61. def OAI.MUB6.Certificate.GramAssembly.Block0.node20 line 212
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node20_check line 214
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node20_eval line 217
  64. def OAI.MUB6.Certificate.GramAssembly.Block0.node21 line 221
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node21_check line 223
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node21_eval line 226
  67. def OAI.MUB6.Certificate.GramAssembly.Block0.node22 line 230
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node22_check line 232
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node22_eval line 235
  70. def OAI.MUB6.Certificate.GramAssembly.Block0.node23 line 240
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node23_check line 242
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block0.node23_eval line 245