OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows8.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source64line 8 - theorem
OAI.MUB6.TaoCertificate.source64_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source64_zeroline 13 - def
OAI.MUB6.TaoCertificate.source65line 23 - theorem
OAI.MUB6.TaoCertificate.source65_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source65_zeroline 28 - def
OAI.MUB6.TaoCertificate.source66line 38 - theorem
OAI.MUB6.TaoCertificate.source66_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source66_zeroline 43 - def
OAI.MUB6.TaoCertificate.source67line 53 - theorem
OAI.MUB6.TaoCertificate.source67_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source67_zeroline 58 - def
OAI.MUB6.TaoCertificate.source68line 68 - theorem
OAI.MUB6.TaoCertificate.source68_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source68_zeroline 73 - def
OAI.MUB6.TaoCertificate.source69line 83 - theorem
OAI.MUB6.TaoCertificate.source69_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source69_zeroline 88 - def
OAI.MUB6.TaoCertificate.source70line 98 - theorem
OAI.MUB6.TaoCertificate.source70_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source70_zeroline 103 - def
OAI.MUB6.TaoCertificate.source71line 113 - theorem
OAI.MUB6.TaoCertificate.source71_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source71_zeroline 118