OAI/Analysis/FreeWords/HaarSignedWords.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.SameSign line 44
  2. theorem OAI.KKFreeWords.SameSign.symm line 46
  3. theorem OAI.KKFreeWords.SameSign.trans line 49
  4. theorem OAI.KKFreeWords.SameSign.add_left line 57
  5. theorem OAI.KKFreeWords.SameSign.add_right line 60
  6. theorem OAI.KKFreeWords.SameSign.nonzero_left line 63
  7. def OAI.KKFreeWords.SignedRelation line 66
  8. def OAI.KKFreeWords.signedWord line 69
  9. def OAI.KKFreeWords.signedExpansion line 72
  10. theorem OAI.KKFreeWords.signedExpansion_value line 76
  11. theorem OAI.KKFreeWords.signedExpansion_chain line 87
  12. theorem OAI.KKFreeWords.signedExpansion_end_chain line 98
  13. theorem OAI.KKFreeWords.signedExpansion_centered line 109
  14. theorem OAI.KKFreeWords.trace_signedWord_centered line 121
  15. theorem OAI.KKFreeWords.trace_signedWord_end line 134
  16. theorem OAI.KKFreeWords.signedChain_center line 151
  17. theorem OAI.KKFreeWords.signedChain_merge line 167