OAI/Analysis/FreeWords/ConjugateFree.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.upow line 36
  2. theorem OAI.KKFreeWords.upow_zero line 38
  3. theorem OAI.KKFreeWords.upow_one line 40
  4. theorem OAI.KKFreeWords.upow_add line 42
  5. theorem OAI.KKFreeWords.upow_neg_mul line 45
  6. theorem OAI.KKFreeWords.upow_mul_neg line 48
  7. theorem OAI.KKFreeWords.star_upow line 51
  8. theorem OAI.KKFreeWords.upow_mem line 56
  9. def OAI.KKFreeWords.conjugate line 70
  10. theorem OAI.KKFreeWords.conjugate_apply line 73
  11. theorem OAI.KKFreeWords.conjugate_inverse line 79
  12. theorem OAI.KKFreeWords.trace_conjugate line 89
  13. def OAI.KKFreeWords.powerWord line 98
  14. def OAI.KKFreeWords.separatedWord line 101
  15. def OAI.KKFreeWords.expandedWord line 106
  16. theorem OAI.KKFreeWords.powerWord_value line 110
  17. theorem OAI.KKFreeWords.separatedWord_head line 114
  18. theorem OAI.KKFreeWords.separatedWord_ne_nil line 118
  19. theorem OAI.KKFreeWords.separatedWord_value line 122
  20. theorem OAI.KKFreeWords.expandedWord_value line 136
  21. def OAI.KKFreeWords.binaryCopy line 146
  22. theorem OAI.KKFreeWords.separatedWord_chain line 149
  23. theorem OAI.KKFreeWords.expandedWord_chain line 162
  24. theorem OAI.KKFreeWords.powerWord_centered line 174
  25. theorem OAI.KKFreeWords.separatedWord_centered line 185
  26. theorem OAI.KKFreeWords.expandedWord_centered line 210
  27. theorem OAI.KKFreeWords.trace_conjugate_word line 223
  28. def OAI.KKFreeWords.conjugateCopy line 239
  29. theorem OAI.KKFreeWords.conjugates_scalarFree line 242
  30. theorem OAI.KKFreeWords.ScalarFree.mono line 268
  31. theorem OAI.KKFreeWords.ScalarFree.reindex line 273