OAI/InformationTheory/Entanglement/ParityData.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteConstruction.Four line 10
  2. abbrev OAI.FiniteConstruction.Outcome line 11
  3. def OAI.FiniteConstruction.XQ line 12
  4. def OAI.FiniteConstruction.ZQ line 13
  5. def OAI.FiniteConstruction.JQ line 14
  6. def OAI.FiniteConstruction.squareQ line 15
  7. def OAI.FiniteConstruction.contextQ line 19
  8. def OAI.FiniteConstruction.signQ line 22
  9. def OAI.FiniteConstruction.eQ line 23
  10. def OAI.FiniteConstruction.hQ line 24
  11. def OAI.FiniteConstruction.eigSignQ line 26
  12. lemma OAI.FiniteConstruction.hQ_symmetric line 29
  13. lemma OAI.FiniteConstruction.hQ_idempotent line 32
  14. lemma OAI.FiniteConstruction.hQ_orthogonal line 35
  15. lemma OAI.FiniteConstruction.hQ_complete line 38
  16. lemma OAI.FiniteConstruction.hQ_eigen line 41
  17. def OAI.FiniteConstruction.h line 46
  18. def OAI.FiniteConstruction.context line 47
  19. def OAI.FiniteConstruction.eigSign line 48