OAI/GroupTheory/PolycyclicRecognition/Algebra/IrreducibleDominantFreePair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A free pair from one two-sided dominant element

For an irreducible real representation of an irreducible polynomial group, generic position supplies the conjugator. The two-sided spectral estimates then give freely generating powers of the element and that conjugate.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.realContinuousRepresentation line 19
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.realContinuousRepresentation_apply line 25
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.free_conjugate_powers_of_irreducible_dominant_element line 29