OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row8.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_0 line 13
  2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_0 line 15
  3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_0 line 19
  4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_0 line 38
  5. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_1 line 45
  6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_1 line 47
  7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_1 line 51
  8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_1 line 70
  9. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_2 line 77
  10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_2 line 79
  11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_2 line 83
  12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_2 line 102
  13. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_3 line 109
  14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_3 line 111
  15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_3 line 115
  16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_3 line 134
  17. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_4 line 141
  18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_4 line 143
  19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_4 line 147
  20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_4 line 166
  21. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_5 line 173
  22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_5 line 175
  23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_5 line 179
  24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_5 line 198
  25. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_6 line 205
  26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_6 line 207
  27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_6 line 211
  28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_6 line 230
  29. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_7 line 237
  30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_7 line 239
  31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_7 line 243
  32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_7 line 262
  33. def OAI.MUB6.Certificate.GramEntries.Block1.rows8_8 line 269
  34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck8_8 line 271
  35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound8_8 line 275
  36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval8_8 line 294