OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows32.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source256line 8 - theorem
OAI.MUB6.TaoCertificate.source256_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source256_zeroline 13 - def
OAI.MUB6.TaoCertificate.source257line 23 - theorem
OAI.MUB6.TaoCertificate.source257_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source257_zeroline 28 - def
OAI.MUB6.TaoCertificate.source258line 38 - theorem
OAI.MUB6.TaoCertificate.source258_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source258_zeroline 43 - def
OAI.MUB6.TaoCertificate.source259line 53 - theorem
OAI.MUB6.TaoCertificate.source259_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source259_zeroline 58 - def
OAI.MUB6.TaoCertificate.source260line 68 - theorem
OAI.MUB6.TaoCertificate.source260_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source260_zeroline 73 - def
OAI.MUB6.TaoCertificate.source261line 83 - theorem
OAI.MUB6.TaoCertificate.source261_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source261_zeroline 88 - def
OAI.MUB6.TaoCertificate.source262line 98 - theorem
OAI.MUB6.TaoCertificate.source262_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source262_zeroline 103 - def
OAI.MUB6.TaoCertificate.source263line 113 - theorem
OAI.MUB6.TaoCertificate.source263_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source263_zeroline 118