OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows2.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source16line 8 - theorem
OAI.MUB6.TaoCertificate.source16_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source16_zeroline 13 - def
OAI.MUB6.TaoCertificate.source17line 23 - theorem
OAI.MUB6.TaoCertificate.source17_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source17_zeroline 28 - def
OAI.MUB6.TaoCertificate.source18line 38 - theorem
OAI.MUB6.TaoCertificate.source18_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source18_zeroline 43 - def
OAI.MUB6.TaoCertificate.source19line 53 - theorem
OAI.MUB6.TaoCertificate.source19_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source19_zeroline 58 - def
OAI.MUB6.TaoCertificate.source20line 68 - theorem
OAI.MUB6.TaoCertificate.source20_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source20_zeroline 73 - def
OAI.MUB6.TaoCertificate.source21line 83 - theorem
OAI.MUB6.TaoCertificate.source21_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source21_zeroline 88 - def
OAI.MUB6.TaoCertificate.source22line 98 - theorem
OAI.MUB6.TaoCertificate.source22_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source22_zeroline 103 - def
OAI.MUB6.TaoCertificate.source23line 113 - theorem
OAI.MUB6.TaoCertificate.source23_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source23_zeroline 118