OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialConjugationSpectrum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Unit-modulus conjugation characters in polynomial-growth groups

Apply the short-word count to powers of the conjugating element and then to its inverse. Every nonzero scalar character of this action has modulus one.

  1. theorem OAI.PolycyclicRecognition.conjugation_character_pow line 16
  2. theorem OAI.PolycyclicRecognition.polynomial_growth_conjugation_character_norm_le_one line 27
  3. theorem OAI.PolycyclicRecognition.polynomial_growth_conjugation_character_norm_eq_one line 42