OAI/Geometry/NilpotentCharts/CentralWords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Polynomial commutator words and rational central spans.

  1. inductive OAI.RawCentralWords.Word line 14
  2. def OAI.RawCentralWords.Word.eval line 22
  3. lemma OAI.RawCentralWords.Word.eval_one line 29
  4. lemma OAI.RawCentralWords.Word.eval_mem line 37
  5. lemma OAI.RawCentralWords.Word.eval_subgroup line 46
  6. def OAI.RawCentralWords.wordSubgroup line 58
  7. lemma OAI.RawCentralWords.wordSubgroup_eq line 67
  8. lemma OAI.RawCentralWords.exists_word line 80
  9. lemma OAI.RawCentralWords.Word.isPoly_eval line 90
  10. lemma OAI.RawCentralWords.Word.isPoly_coords_eval line 103
  11. def OAI.RawCentralWords.wordLog line 118
  12. lemma OAI.RawCentralWords.wordLog_poly line 122
  13. lemma OAI.RawCentralWords.coord_symm_zero line 127
  14. lemma OAI.RawCentralWords.wordLog_zero line 133
  15. def OAI.RawCentralWords.centralWordSpan line 140
  16. lemma OAI.RawCentralWords.wordLog_map line 149
  17. def OAI.RawCentralWords.vectorSubgroup line 154
  18. lemma OAI.RawCentralWords.vectorSubgroup_closed line 158
  19. lemma OAI.RawCentralWords.centralWordSpan_closure line 172
  20. lemma OAI.RawCentralWords.centralWordSpan_lattice_span line 213