OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows0.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source0line 8 - theorem
OAI.MUB6.TaoCertificate.source0_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source0_zeroline 13 - def
OAI.MUB6.TaoCertificate.source1line 23 - theorem
OAI.MUB6.TaoCertificate.source1_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source1_zeroline 28 - def
OAI.MUB6.TaoCertificate.source2line 38 - theorem
OAI.MUB6.TaoCertificate.source2_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source2_zeroline 43 - def
OAI.MUB6.TaoCertificate.source3line 53 - theorem
OAI.MUB6.TaoCertificate.source3_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source3_zeroline 58 - def
OAI.MUB6.TaoCertificate.source4line 68 - theorem
OAI.MUB6.TaoCertificate.source4_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source4_zeroline 73 - def
OAI.MUB6.TaoCertificate.source5line 83 - theorem
OAI.MUB6.TaoCertificate.source5_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source5_zeroline 88 - def
OAI.MUB6.TaoCertificate.source6line 98 - theorem
OAI.MUB6.TaoCertificate.source6_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source6_zeroline 103 - def
OAI.MUB6.TaoCertificate.source7line 113 - theorem
OAI.MUB6.TaoCertificate.source7_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source7_zeroline 118