OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Reindex4.lean
23 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_0line 9 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_1line 13 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_2line 17 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_3line 21 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_4line 25 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_5line 29 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_6line 33 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_7line 37 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_8line 41 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_9line 45 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_10line 49 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_11line 53 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_12line 57 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_13line 61 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_14line 65 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_15line 69 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_16line 73 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_17line 77 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_18line 81 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_19line 85 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_20line 89 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entry_reindex_4_21line 93 - theorem
OAI.MUB6.Certificate.GramAssembly.Block4.entries_reindex_4line 97