OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteRationalRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A uniform bound for finite faithful rational representations

The integral lattice is the span of the finite orbit of a rational basis. Reduction modulo three then bounds the group order.

  1. def OAI.PolycyclicRecognition.finiteOrbitIntegerLattice line 18
  2. theorem OAI.PolycyclicRecognition.finiteOrbitIntegerLattice_basis_mem line 22
  3. theorem OAI.PolycyclicRecognition.finiteOrbitIntegerLattice_isLattice line 27
  4. theorem OAI.PolycyclicRecognition.finiteOrbitIntegerLattice_stable line 38
  5. def OAI.PolycyclicRecognition.finiteOrbitIntegerRepresentation line 53
  6. theorem OAI.PolycyclicRecognition.finiteOrbitIntegerRepresentation_injective line 63
  7. theorem OAI.PolycyclicRecognition.finite_rational_representation_card_le line 73