OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row7.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_0 line 19
  2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_0 line 21
  3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_0 line 25
  4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_0 line 60
  5. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_1 line 67
  6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_1 line 69
  7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_1 line 73
  8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_1 line 108
  9. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_2 line 115
  10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_2 line 117
  11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_2 line 121
  12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_2 line 156
  13. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_3 line 163
  14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_3 line 165
  15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_3 line 169
  16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_3 line 204
  17. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_4 line 211
  18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_4 line 213
  19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_4 line 217
  20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_4 line 252
  21. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_5 line 259
  22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_5 line 261
  23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_5 line 265
  24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_5 line 300
  25. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_6 line 307
  26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_6 line 309
  27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_6 line 313
  28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_6 line 348
  29. def OAI.MUB6.Certificate.GramEntries.Block1.rows7_7 line 355
  30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck7_7 line 357
  31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound7_7 line 361
  32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval7_7 line 396