OAI/GroupTheory/PolycyclicRecognition/Algebra/PrimitiveWordProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The Dynkin projection identity for primitive rational words

  1. theorem OAI.PolycyclicRecognition.rationalWordDegree_one line 15
  2. theorem OAI.PolycyclicRecognition.rationalWordAntipode_one line 19
  3. theorem OAI.PolycyclicRecognition.wordAntipodeConvolution_coproduct line 24
  4. theorem OAI.PolycyclicRecognition.wordDegreeConvolution_coproduct line 49
  5. theorem OAI.PolycyclicRecognition.IsPrimitiveRationalWord.projection_eq_degree line 76

    Source documentation

    Primitive words are sent to their degree derivative by the Dynkin projection.

    theorem IsPrimitiveRationalWord.projection_eq_degree {p : RationalWords n}
    (hp : IsPrimitiveRationalWord p) :
    wordLieProjection rationalWordLetter p = rationalWordDegree p := by
…

    Mentions: OAI.PolycyclicRecognition.RationalWords, OAI.PolycyclicRecognition.IsPrimitiveRationalWord, OAI.PolycyclicRecognition.wordLieProjection, OAI.PolycyclicRecognition.rationalWordLetter, OAI.PolycyclicRecognition.rationalWordDegree