OAI/Analysis/MutuallyUnbiased/Certificate/GramPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite auxiliary Gram products interpreted as sparse normalized keys.

  1. def OAI.MUB6.Certificate.GramPolynomial.compareRows line 12
  2. def OAI.MUB6.Certificate.GramPolynomial.keyLess line 19
  3. def OAI.MUB6.Certificate.GramPolynomial.normalizedRow line 23
  4. theorem OAI.MUB6.Certificate.GramPolynomial.normalizedRow_eval line 27
  5. theorem OAI.MUB6.Certificate.GramPolynomial.mixedGram_eq_rows line 35
  6. theorem OAI.MUB6.Certificate.GramPolynomial.mixedGram_symm line 48
  7. theorem OAI.MUB6.Certificate.GramPolynomial.collectWeightedRows_eval line 53