OAI/Analysis/MutuallyUnbiased/GramFunctions/Block0.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramFunctions.Block0.shape line 7
2. def OAI.MUB6.Certificate.GramFunctions.Block0.decimalExponent line 8
3. def OAI.MUB6.Certificate.GramFunctions.Block0.seed0 line 10
4. def OAI.MUB6.Certificate.GramFunctions.Block0.terms0 line 12
5. def OAI.MUB6.Certificate.GramFunctions.Block0.form0 line 57
6. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced0 line 59
7. def OAI.MUB6.Certificate.GramFunctions.Block0.seed1 line 64
8. def OAI.MUB6.Certificate.GramFunctions.Block0.terms1 line 66
9. def OAI.MUB6.Certificate.GramFunctions.Block0.form1 line 111
10. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced1 line 113
11. def OAI.MUB6.Certificate.GramFunctions.Block0.seed2 line 118
12. def OAI.MUB6.Certificate.GramFunctions.Block0.terms2 line 120
13. def OAI.MUB6.Certificate.GramFunctions.Block0.form2 line 165
14. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced2 line 167
15. def OAI.MUB6.Certificate.GramFunctions.Block0.seed3 line 172
16. def OAI.MUB6.Certificate.GramFunctions.Block0.terms3 line 174
17. def OAI.MUB6.Certificate.GramFunctions.Block0.form3 line 219
18. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced3 line 221
19. def OAI.MUB6.Certificate.GramFunctions.Block0.seed4 line 226
20. def OAI.MUB6.Certificate.GramFunctions.Block0.terms4 line 228
21. def OAI.MUB6.Certificate.GramFunctions.Block0.form4 line 273
22. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced4 line 275
23. def OAI.MUB6.Certificate.GramFunctions.Block0.forms line 280
24. theorem OAI.MUB6.Certificate.GramFunctions.Block0.balanced line 283