OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows5.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source40line 8 - theorem
OAI.MUB6.TaoCertificate.source40_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source40_zeroline 13 - def
OAI.MUB6.TaoCertificate.source41line 23 - theorem
OAI.MUB6.TaoCertificate.source41_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source41_zeroline 28 - def
OAI.MUB6.TaoCertificate.source42line 38 - theorem
OAI.MUB6.TaoCertificate.source42_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source42_zeroline 43 - def
OAI.MUB6.TaoCertificate.source43line 53 - theorem
OAI.MUB6.TaoCertificate.source43_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source43_zeroline 58 - def
OAI.MUB6.TaoCertificate.source44line 68 - theorem
OAI.MUB6.TaoCertificate.source44_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source44_zeroline 73 - def
OAI.MUB6.TaoCertificate.source45line 83 - theorem
OAI.MUB6.TaoCertificate.source45_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source45_zeroline 88 - def
OAI.MUB6.TaoCertificate.source46line 98 - theorem
OAI.MUB6.TaoCertificate.source46_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source46_zeroline 103 - def
OAI.MUB6.TaoCertificate.source47line 113 - theorem
OAI.MUB6.TaoCertificate.source47_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source47_zeroline 118