OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row7.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_0 line 15
  2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_0 line 17
  3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_0 line 21
  4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_0 line 50
  5. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_1 line 57
  6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_1 line 59
  7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_1 line 63
  8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_1 line 92
  9. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_2 line 99
  10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_2 line 101
  11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_2 line 105
  12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_2 line 134
  13. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_3 line 141
  14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_3 line 143
  15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_3 line 147
  16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_3 line 176
  17. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_4 line 183
  18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_4 line 185
  19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_4 line 189
  20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_4 line 218
  21. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_5 line 225
  22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_5 line 227
  23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_5 line 231
  24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_5 line 260
  25. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_6 line 267
  26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_6 line 269
  27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_6 line 273
  28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_6 line 302
  29. def OAI.MUB6.Certificate.GramEntries.Block3.rows7_7 line 309
  30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck7_7 line 311
  31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound7_7 line 315
  32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval7_7 line 344