OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentConjugationWords.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A common dimension bound for mixed conjugation differences

Nilpotence of the group annihilates sufficiently long products even when successive conjugating elements differ. The action filtration improves this bound to the rational rank of the abelian normal subgroup.

  1. theorem OAI.PolycyclicRecognition.integralConjugationWord_mem line 20
  2. theorem OAI.PolycyclicRecognition.integralConjugationWord_zero line 31
  3. theorem OAI.PolycyclicRecognition.rationalConjugationWord_baseChange line 42
  4. theorem OAI.PolycyclicRecognition.rationalConjugationWord_zero_at_rank line 53