OAI/GroupTheory/PolycyclicRecognition/Analysis/ControlledChainGenerators.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite group-ring generators at a fixed scale

Normalizing the first vertex to the identity leaves only finitely many tuples. Their translates generate all chains at the chosen scale.

  1. theorem OAI.PolycyclicRecognition.finite_normalizedControlledTuples line 17
  2. theorem OAI.PolycyclicRecognition.controlledChainSubrepresentation_fg line 23