OAI/Analysis/MutuallyUnbiased/GramEntries/Block0Data.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramEntries.Block0.entry0_0 line 23
  2. def OAI.MUB6.Certificate.GramEntries.Block0.entry1_0 line 25
  3. def OAI.MUB6.Certificate.GramEntries.Block0.entry1_1 line 27
  4. def OAI.MUB6.Certificate.GramEntries.Block0.entry2_0 line 29
  5. def OAI.MUB6.Certificate.GramEntries.Block0.entry2_1 line 31
  6. def OAI.MUB6.Certificate.GramEntries.Block0.entry2_2 line 33
  7. def OAI.MUB6.Certificate.GramEntries.Block0.entry3_0 line 35
  8. def OAI.MUB6.Certificate.GramEntries.Block0.entry3_1 line 37
  9. def OAI.MUB6.Certificate.GramEntries.Block0.entry3_2 line 39
  10. def OAI.MUB6.Certificate.GramEntries.Block0.entry3_3 line 41
  11. def OAI.MUB6.Certificate.GramEntries.Block0.entry4_0 line 43
  12. def OAI.MUB6.Certificate.GramEntries.Block0.entry4_1 line 45
  13. def OAI.MUB6.Certificate.GramEntries.Block0.entry4_2 line 47
  14. def OAI.MUB6.Certificate.GramEntries.Block0.entry4_3 line 49
  15. def OAI.MUB6.Certificate.GramEntries.Block0.entry4_4 line 51
  16. def OAI.MUB6.Certificate.GramEntries.Block0.entries line 53