OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows10.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source80line 8 - theorem
OAI.MUB6.TaoCertificate.source80_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source80_zeroline 13 - def
OAI.MUB6.TaoCertificate.source81line 23 - theorem
OAI.MUB6.TaoCertificate.source81_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source81_zeroline 28 - def
OAI.MUB6.TaoCertificate.source82line 38 - theorem
OAI.MUB6.TaoCertificate.source82_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source82_zeroline 43 - def
OAI.MUB6.TaoCertificate.source83line 53 - theorem
OAI.MUB6.TaoCertificate.source83_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source83_zeroline 58 - def
OAI.MUB6.TaoCertificate.source84line 68 - theorem
OAI.MUB6.TaoCertificate.source84_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source84_zeroline 73 - def
OAI.MUB6.TaoCertificate.source85line 83 - theorem
OAI.MUB6.TaoCertificate.source85_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source85_zeroline 88 - def
OAI.MUB6.TaoCertificate.source86line 98 - theorem
OAI.MUB6.TaoCertificate.source86_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source86_zeroline 103 - def
OAI.MUB6.TaoCertificate.source87line 113 - theorem
OAI.MUB6.TaoCertificate.source87_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source87_zeroline 118