OAI/Analysis/FreeWords/FlipBasic.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KKFreeLiftDiagnostic.Block line 13
  2. def OAI.KKFreeLiftDiagnostic.flip line 15
  3. def OAI.KKFreeLiftDiagnostic.left line 17
  4. def OAI.KKFreeLiftDiagnostic.partialTrace line 19
  5. def OAI.KKFreeLiftDiagnostic.normalizedTrace line 22
  6. def OAI.KKFreeLiftDiagnostic.centeredFlip line 25
  7. def OAI.KKFreeLiftDiagnostic.mixedWord line 27
  8. def OAI.KKFreeLiftDiagnostic.right line 30
  9. theorem OAI.KKFreeLiftDiagnostic.mul_flip line 32
  10. theorem OAI.KKFreeLiftDiagnostic.flip_mul line 37
  11. theorem OAI.KKFreeLiftDiagnostic.flip_mul_flip line 46
  12. theorem OAI.KKFreeLiftDiagnostic.flip_star line 50
  13. theorem OAI.KKFreeLiftDiagnostic.flip_unitary line 56
  14. theorem OAI.KKFreeLiftDiagnostic.flip_left_flip line 59
  15. theorem OAI.KKFreeLiftDiagnostic.left_star line 64
  16. theorem OAI.KKFreeLiftDiagnostic.left_unitary line 69
  17. theorem OAI.KKFreeLiftDiagnostic.mixedWord_flip line 81
  18. theorem OAI.KKFreeLiftDiagnostic.partialTrace_sub line 98
  19. theorem OAI.KKFreeLiftDiagnostic.partialTrace_smul line 103
  20. theorem OAI.KKFreeLiftDiagnostic.partialTrace_one line 108
  21. theorem OAI.KKFreeLiftDiagnostic.partialTrace_flip line 117
  22. theorem OAI.KKFreeLiftDiagnostic.partialTrace_centeredFlip line 126
  23. theorem OAI.KKFreeLiftDiagnostic.trace_flip line 130
  24. theorem OAI.KKFreeLiftDiagnostic.normalizedTrace_one line 135
  25. theorem OAI.KKFreeLiftDiagnostic.normalizedTrace_centeredFlip line 141