OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows13.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source104line 8 - theorem
OAI.MUB6.TaoCertificate.source104_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source104_zeroline 13 - def
OAI.MUB6.TaoCertificate.source105line 23 - theorem
OAI.MUB6.TaoCertificate.source105_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source105_zeroline 28 - def
OAI.MUB6.TaoCertificate.source106line 38 - theorem
OAI.MUB6.TaoCertificate.source106_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source106_zeroline 43 - def
OAI.MUB6.TaoCertificate.source107line 53 - theorem
OAI.MUB6.TaoCertificate.source107_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source107_zeroline 58 - def
OAI.MUB6.TaoCertificate.source108line 68 - theorem
OAI.MUB6.TaoCertificate.source108_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source108_zeroline 73 - def
OAI.MUB6.TaoCertificate.source109line 83 - theorem
OAI.MUB6.TaoCertificate.source109_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source109_zeroline 88 - def
OAI.MUB6.TaoCertificate.source110line 98 - theorem
OAI.MUB6.TaoCertificate.source110_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source110_zeroline 103 - def
OAI.MUB6.TaoCertificate.source111line 113 - theorem
OAI.MUB6.TaoCertificate.source111_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source111_zeroline 118