OAI/Analysis/MutuallyUnbiased/GramData/Block4Data.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Exact integer matrix for λ = (2, 3), m = 22, exponent = 14.

  1. def OAI.MUB6.Certificate.GramData.Block4.Z line 14
  2. def OAI.MUB6.Certificate.GramData.Block4.entries line 39
  3. def OAI.MUB6.Certificate.GramData.Block4.D line 64
  4. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_0 line 66
  5. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_1 line 68
  6. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_2 line 70
  7. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_3 line 72
  8. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_4 line 74
  9. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_5 line 76
  10. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_6 line 78
  11. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_7 line 80
  12. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_8 line 82
  13. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_9 line 84
  14. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_10 line 86
  15. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_11 line 88
  16. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_12 line 90
  17. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_13 line 92
  18. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_14 line 94
  19. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_15 line 96
  20. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_16 line 98
  21. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_17 line 100
  22. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_18 line 102
  23. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_19 line 104
  24. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_20 line 106
  25. theorem OAI.MUB6.Certificate.GramData.Block4.pivot_21 line 108