OAI/Analysis/FreeWords/HaarTwistLetters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.signInt line 72
  2. def OAI.KKFreeWords.unitaryLetter line 74
  3. def OAI.KKFreeWords.twistLeft line 76
  4. def OAI.KKFreeWords.twistRight line 78
  5. def OAI.KKFreeWords.letterWord line 80
  6. def OAI.KKFreeWords.twistExpansion line 83
  7. theorem OAI.KKFreeWords.unitaryLetter_factor line 90
  8. theorem OAI.KKFreeWords.twistLeft_mem line 95
  9. theorem OAI.KKFreeWords.twistRight_mem line 102
  10. theorem OAI.KKFreeWords.twistExpansion_mem line 109
  11. def OAI.KKFreeWords.LetterRelation line 132
  12. theorem OAI.KKFreeWords.trace_unitarySandwich line 136
  13. theorem OAI.KKFreeWords.twist_separator_relation line 143
  14. theorem OAI.KKFreeWords.twistExpansion_chain line 156
  15. theorem OAI.KKFreeWords.twistExpansion_value line 178
  16. theorem OAI.KKFreeWords.twistExpansion_right line 202
  17. theorem OAI.KKFreeWords.trace_letterWord line 217