OAI/Analysis/MutuallyUnbiased/GramData/Block0.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (1, 1, 1, 2), m = 5, exponent = 14.

  1. def OAI.MUB6.Certificate.GramData.Block0.Z line 14
  2. def OAI.MUB6.Certificate.GramData.Block0.entries line 22
  3. def OAI.MUB6.Certificate.GramData.Block0.D line 30
  4. theorem OAI.MUB6.Certificate.GramData.Block0.pivot_0 line 32
  5. theorem OAI.MUB6.Certificate.GramData.Block0.pivot_1 line 34
  6. theorem OAI.MUB6.Certificate.GramData.Block0.pivot_2 line 36
  7. theorem OAI.MUB6.Certificate.GramData.Block0.pivot_3 line 38
  8. theorem OAI.MUB6.Certificate.GramData.Block0.pivot_4 line 40
  9. theorem OAI.MUB6.Certificate.GramData.Block0.entry_0_0 line 42
  10. theorem OAI.MUB6.Certificate.GramData.Block0.entry_0_1 line 46
  11. theorem OAI.MUB6.Certificate.GramData.Block0.entry_0_2 line 50
  12. theorem OAI.MUB6.Certificate.GramData.Block0.entry_0_3 line 54
  13. theorem OAI.MUB6.Certificate.GramData.Block0.entry_0_4 line 58
  14. theorem OAI.MUB6.Certificate.GramData.Block0.entry_1_0 line 62
  15. theorem OAI.MUB6.Certificate.GramData.Block0.entry_1_1 line 66
  16. theorem OAI.MUB6.Certificate.GramData.Block0.entry_1_2 line 70
  17. theorem OAI.MUB6.Certificate.GramData.Block0.entry_1_3 line 74
  18. theorem OAI.MUB6.Certificate.GramData.Block0.entry_1_4 line 78
  19. theorem OAI.MUB6.Certificate.GramData.Block0.entry_2_0 line 82
  20. theorem OAI.MUB6.Certificate.GramData.Block0.entry_2_1 line 86
  21. theorem OAI.MUB6.Certificate.GramData.Block0.entry_2_2 line 90
  22. theorem OAI.MUB6.Certificate.GramData.Block0.entry_2_3 line 94
  23. theorem OAI.MUB6.Certificate.GramData.Block0.entry_2_4 line 98
  24. theorem OAI.MUB6.Certificate.GramData.Block0.entry_3_0 line 102
  25. theorem OAI.MUB6.Certificate.GramData.Block0.entry_3_1 line 106
  26. theorem OAI.MUB6.Certificate.GramData.Block0.entry_3_2 line 110
  27. theorem OAI.MUB6.Certificate.GramData.Block0.entry_3_3 line 114
  28. theorem OAI.MUB6.Certificate.GramData.Block0.entry_3_4 line 118
  29. theorem OAI.MUB6.Certificate.GramData.Block0.entry_4_0 line 122
  30. theorem OAI.MUB6.Certificate.GramData.Block0.entry_4_1 line 126
  31. theorem OAI.MUB6.Certificate.GramData.Block0.entry_4_2 line 130
  32. theorem OAI.MUB6.Certificate.GramData.Block0.entry_4_3 line 134
  33. theorem OAI.MUB6.Certificate.GramData.Block0.entry_4_4 line 138
  34. theorem OAI.MUB6.Certificate.GramData.Block0.pivots_pos line 142
  35. theorem OAI.MUB6.Certificate.GramData.Block0.gram line 151
  36. theorem OAI.MUB6.Certificate.GramData.Block0.positiveDefinite line 181