OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows1.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source8line 8 - theorem
OAI.MUB6.TaoCertificate.source8_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source8_zeroline 13 - def
OAI.MUB6.TaoCertificate.source9line 23 - theorem
OAI.MUB6.TaoCertificate.source9_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source9_zeroline 28 - def
OAI.MUB6.TaoCertificate.source10line 38 - theorem
OAI.MUB6.TaoCertificate.source10_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source10_zeroline 43 - def
OAI.MUB6.TaoCertificate.source11line 53 - theorem
OAI.MUB6.TaoCertificate.source11_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source11_zeroline 58 - def
OAI.MUB6.TaoCertificate.source12line 68 - theorem
OAI.MUB6.TaoCertificate.source12_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source12_zeroline 73 - def
OAI.MUB6.TaoCertificate.source13line 83 - theorem
OAI.MUB6.TaoCertificate.source13_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source13_zeroline 88 - def
OAI.MUB6.TaoCertificate.source14line 98 - theorem
OAI.MUB6.TaoCertificate.source14_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source14_zeroline 103 - def
OAI.MUB6.TaoCertificate.source15line 113 - theorem
OAI.MUB6.TaoCertificate.source15_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source15_zeroline 118