OAI/Analysis/MutuallyUnbiased/TaoCertificate/Rows25.lean
24 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.TaoCertificate.source200line 8 - theorem
OAI.MUB6.TaoCertificate.source200_checkedline 10 - theorem
OAI.MUB6.TaoCertificate.source200_zeroline 13 - def
OAI.MUB6.TaoCertificate.source201line 23 - theorem
OAI.MUB6.TaoCertificate.source201_checkedline 25 - theorem
OAI.MUB6.TaoCertificate.source201_zeroline 28 - def
OAI.MUB6.TaoCertificate.source202line 38 - theorem
OAI.MUB6.TaoCertificate.source202_checkedline 40 - theorem
OAI.MUB6.TaoCertificate.source202_zeroline 43 - def
OAI.MUB6.TaoCertificate.source203line 53 - theorem
OAI.MUB6.TaoCertificate.source203_checkedline 55 - theorem
OAI.MUB6.TaoCertificate.source203_zeroline 58 - def
OAI.MUB6.TaoCertificate.source204line 68 - theorem
OAI.MUB6.TaoCertificate.source204_checkedline 70 - theorem
OAI.MUB6.TaoCertificate.source204_zeroline 73 - def
OAI.MUB6.TaoCertificate.source205line 83 - theorem
OAI.MUB6.TaoCertificate.source205_checkedline 85 - theorem
OAI.MUB6.TaoCertificate.source205_zeroline 88 - def
OAI.MUB6.TaoCertificate.source206line 98 - theorem
OAI.MUB6.TaoCertificate.source206_checkedline 100 - theorem
OAI.MUB6.TaoCertificate.source206_zeroline 103 - def
OAI.MUB6.TaoCertificate.source207line 113 - theorem
OAI.MUB6.TaoCertificate.source207_checkedline 115 - theorem
OAI.MUB6.TaoCertificate.source207_zeroline 118