OAI/Analysis/MutuallyUnbiased/GramEntries/Block5Row8.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_0 line 12
  2. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_0 line 14
  3. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_0 line 18
  4. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_0 line 28
  5. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_1 line 35
  6. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_1 line 37
  7. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_1 line 41
  8. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_1 line 51
  9. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_2 line 58
  10. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_2 line 60
  11. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_2 line 64
  12. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_2 line 74
  13. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_3 line 81
  14. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_3 line 83
  15. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_3 line 87
  16. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_3 line 97
  17. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_4 line 104
  18. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_4 line 106
  19. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_4 line 110
  20. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_4 line 120
  21. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_5 line 127
  22. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_5 line 129
  23. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_5 line 133
  24. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_5 line 143
  25. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_6 line 150
  26. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_6 line 152
  27. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_6 line 156
  28. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_6 line 166
  29. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_7 line 173
  30. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_7 line 175
  31. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_7 line 179
  32. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_7 line 189
  33. def OAI.MUB6.Certificate.GramEntries.Block5.rows8_8 line 196
  34. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck8_8 line 198
  35. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound8_8 line 202
  36. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval8_8 line 212