OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows30.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source240line 8 - theorem
OAI.MUB6.TaoCertificate.source240_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source240_zeroline 13 - def
OAI.MUB6.TaoCertificate.source241line 23 - theorem
OAI.MUB6.TaoCertificate.source241_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source241_zeroline 28 - def
OAI.MUB6.TaoCertificate.source242line 38 - theorem
OAI.MUB6.TaoCertificate.source242_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source242_zeroline 43 - def
OAI.MUB6.TaoCertificate.source243line 53 - theorem
OAI.MUB6.TaoCertificate.source243_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source243_zeroline 58 - def
OAI.MUB6.TaoCertificate.source244line 68 - theorem
OAI.MUB6.TaoCertificate.source244_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source244_zeroline 73 - def
OAI.MUB6.TaoCertificate.source245line 83 - theorem
OAI.MUB6.TaoCertificate.source245_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source245_zeroline 88 - def
OAI.MUB6.TaoCertificate.source246line 98 - theorem
OAI.MUB6.TaoCertificate.source246_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source246_zeroline 103 - def
OAI.MUB6.TaoCertificate.source247line 113 - theorem
OAI.MUB6.TaoCertificate.source247_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source247_zeroline 118