OAI/GroupTheory/PolycyclicRecognition/Algebra/HomogeneousWordProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous primitive words and their right-nested Lie expressions

  1. def OAI.PolycyclicRecognition.IsHomogeneousRationalWord line 13
  2. theorem OAI.PolycyclicRecognition.rationalWordDegree_coeff line 16
  3. theorem OAI.PolycyclicRecognition.IsHomogeneousRationalWord.degree_eq line 32
  4. theorem OAI.PolycyclicRecognition.rationalWordEvaluation_letter line 42
  5. theorem OAI.PolycyclicRecognition.rationalWordEvaluation_wordRightLie line 46
  6. theorem OAI.PolycyclicRecognition.rationalWordEvaluation_projection line 57
  7. theorem OAI.PolycyclicRecognition.primitive_homogeneous_word_projection line 69

    Source documentation

    The degree identity holds after substitution in any rational associative algebra.

    theorem primitive_homogeneous_word_projection {p : RationalWords n} {d : ℕ}
    (hp : IsPrimitiveRationalWord p) (hd : IsHomogeneousRationalWord p d) :
    wordLieProjection X p = (d : ℚ) • rationalWordEvaluation X p := by
…

    Mentions: OAI.PolycyclicRecognition.RationalWords, OAI.PolycyclicRecognition.IsPrimitiveRationalWord, OAI.PolycyclicRecognition.IsHomogeneousRationalWord, OAI.PolycyclicRecognition.wordLieProjection, OAI.PolycyclicRecognition.rationalWordEvaluation