OAI/GroupTheory/PolycyclicRecognition/Algebra/ValuedIrreducibleFreePair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Irreducible valued representations with a two-sided dominant element

The coefficient field may be archimedean or nonarchimedean. Generic position uses its polynomial topology; contraction uses its given norm.

  1. def OAI.PolycyclicRecognition.PolynomialMatrixGroup.valuedContinuousRepresentation line 18
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.valuedContinuousRepresentation_apply line 24
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.free_conjugate_powers_of_irreducible_valued_dominant_element line 28