OAI/GroupTheory/FiniteType/SteinbergWords.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SteinbergWords.interchange line 11
  2. structure OAI.SteinbergWords.Initial line 40
  3. def OAI.SteinbergWords.middle line 51
  4. lemma OAI.SteinbergWords.middle_left line 52
  5. lemma OAI.SteinbergWords.middle_right line 54
  6. def OAI.SteinbergWords.word line 59
  7. lemma OAI.SteinbergWords.word_nil line 66
  8. lemma OAI.SteinbergWords.word_singleton line 68
  9. lemma OAI.SteinbergWords.word_cons_cons line 70
  10. def OAI.SteinbergWords.Away line 77
  11. def OAI.SteinbergWords.Chain line 81
  12. lemma OAI.SteinbergWords.base line 86
  13. lemma OAI.SteinbergWords.split_head line 117
  14. lemma OAI.SteinbergWords.commute_bracket_left line 141
  15. lemma OAI.SteinbergWords.away_step line 145
  16. lemma OAI.SteinbergWords.chain_step line 175
  17. lemma OAI.SteinbergWords.laws line 225
  18. theorem OAI.SteinbergWords.word_commute line 232
  19. theorem OAI.SteinbergWords.word_chain line 237
  20. def OAI.SteinbergWords.rootSubgroup line 241
  21. instance OAI.SteinbergWords.rootSubgroupCommutative line 244
  22. def OAI.SteinbergWords.polynomialAdd line 252
  23. def OAI.SteinbergWords.polynomial line 258
  24. lemma OAI.SteinbergWords.polynomial_of line 261
  25. lemma OAI.SteinbergWords.polynomial_zero line 264
  26. lemma OAI.SteinbergWords.polynomial_add line 266
  27. lemma OAI.SteinbergWords.polynomial_neg line 269
  28. lemma OAI.SteinbergWords.polynomial_commute line 272
  29. lemma OAI.SteinbergWords.bracket_inv_left line 286
  30. lemma OAI.SteinbergWords.bracket_inv_right line 290
  31. lemma OAI.SteinbergWords.bracket_mul_left line 294
  32. lemma OAI.SteinbergWords.bracket_mul_right line 299
  33. theorem OAI.SteinbergWords.polynomial_chain line 304