OAI/Analysis/MutuallyUnbiased/GramAssembly/Block5Reindex0.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_0line 9 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_1line 13 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_2line 17 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_3line 21 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_4line 25 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_5line 29 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_6line 33 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_7line 37 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_8line 41 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_9line 45 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_10line 49 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entry_reindex_0_11line 53 - theorem
OAI.MUB6.Certificate.GramAssembly.Block5.entries_reindex_0line 57