OAI/Analysis/MutuallyUnbiased/PairMoments/PairCharges.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MUB6.qCrossline 11 - def
OAI.MUB6.qSameline 12 - def
OAI.MUB6.pairWline 13 - def
OAI.MUB6.pairAline 14 - def
OAI.MUB6.pairCoefficientline 17 - def
OAI.MUB6.pairLline 19 - def
OAI.MUB6.PairCertificateIdentityline 22 - theorem
OAI.MUB6.pair_product_zero_of_certificateline 26