OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row8.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_0 line 14
  2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_0 line 16
  3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_0 line 20
  4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_0 line 45
  5. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_1 line 52
  6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_1 line 54
  7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_1 line 58
  8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_1 line 83
  9. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_2 line 90
  10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_2 line 92
  11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_2 line 96
  12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_2 line 121
  13. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_3 line 128
  14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_3 line 130
  15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_3 line 134
  16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_3 line 159
  17. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_4 line 166
  18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_4 line 168
  19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_4 line 172
  20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_4 line 197
  21. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_5 line 204
  22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_5 line 206
  23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_5 line 210
  24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_5 line 235
  25. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_6 line 242
  26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_6 line 244
  27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_6 line 248
  28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_6 line 273
  29. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_7 line 280
  30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_7 line 282
  31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_7 line 286
  32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_7 line 311
  33. def OAI.MUB6.Certificate.GramEntries.Block4.rows8_8 line 318
  34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck8_8 line 320
  35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound8_8 line 324
  36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval8_8 line 349