OAI/Analysis/MutuallyUnbiased/GramEntries/Block5Row9.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_0 line 13
  2. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_0 line 15
  3. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_0 line 19
  4. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_0 line 34
  5. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_1 line 41
  6. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_1 line 43
  7. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_1 line 47
  8. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_1 line 62
  9. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_2 line 69
  10. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_2 line 71
  11. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_2 line 75
  12. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_2 line 90
  13. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_3 line 97
  14. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_3 line 99
  15. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_3 line 103
  16. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_3 line 118
  17. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_4 line 125
  18. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_4 line 127
  19. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_4 line 131
  20. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_4 line 146
  21. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_5 line 153
  22. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_5 line 155
  23. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_5 line 159
  24. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_5 line 174
  25. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_6 line 181
  26. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_6 line 183
  27. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_6 line 187
  28. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_6 line 202
  29. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_7 line 209
  30. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_7 line 211
  31. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_7 line 215
  32. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_7 line 230
  33. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_8 line 237
  34. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_8 line 239
  35. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_8 line 243
  36. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_8 line 258
  37. def OAI.MUB6.Certificate.GramEntries.Block5.rows9_9 line 265
  38. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryCheck9_9 line 267
  39. theorem OAI.MUB6.Certificate.GramEntries.Block5.rowsSound9_9 line 271
  40. theorem OAI.MUB6.Certificate.GramEntries.Block5.entryEval9_9 line 286