OAI/Analysis/MutuallyUnbiased/PairMoments/PairCharges.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.qCross line 11
  2. def OAI.MUB6.qSame line 12
  3. def OAI.MUB6.pairW line 13
  4. def OAI.MUB6.pairA line 14
  5. def OAI.MUB6.pairCoefficient line 17
  6. def OAI.MUB6.pairL line 19
  7. def OAI.MUB6.PairCertificateIdentity line 22
  8. theorem OAI.MUB6.pair_product_zero_of_certificate line 26