OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGoodWordPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cartan paths along the good vertices of a conjugated word

The profile on the second sheet is evaluated at n * k. The recurrence word moves n by conjugation, so multiplying its vertices by k gives the ordinary root-generator chain required by the Cartan path theorem.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_good_conjugated_word_paths line 29