OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows7.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source56line 8 - theorem
OAI.MUB6.TaoCertificate.source56_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source56_zeroline 13 - def
OAI.MUB6.TaoCertificate.source57line 23 - theorem
OAI.MUB6.TaoCertificate.source57_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source57_zeroline 28 - def
OAI.MUB6.TaoCertificate.source58line 38 - theorem
OAI.MUB6.TaoCertificate.source58_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source58_zeroline 43 - def
OAI.MUB6.TaoCertificate.source59line 53 - theorem
OAI.MUB6.TaoCertificate.source59_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source59_zeroline 58 - def
OAI.MUB6.TaoCertificate.source60line 68 - theorem
OAI.MUB6.TaoCertificate.source60_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source60_zeroline 73 - def
OAI.MUB6.TaoCertificate.source61line 83 - theorem
OAI.MUB6.TaoCertificate.source61_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source61_zeroline 88 - def
OAI.MUB6.TaoCertificate.source62line 98 - theorem
OAI.MUB6.TaoCertificate.source62_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source62_zeroline 103 - def
OAI.MUB6.TaoCertificate.source63line 113 - theorem
OAI.MUB6.TaoCertificate.source63_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source63_zeroline 118