OAI/GroupTheory/PolycyclicRecognition/Algebra/MonoidModuleAscendingBase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite monoid module supplies the ascending base

The module action uses the nonnegative iterates of the inverse automorphism. Thus its finite generation has the required direction, unlike finite generation over the Laurent group ring.

  1. def OAI.PolycyclicRecognition.integralLinearMulAut line 19
  2. theorem OAI.PolycyclicRecognition.integralLinearMulAut_pow line 22
  3. def OAI.PolycyclicRecognition.inverseIterateRepresentation line 31
  4. theorem OAI.PolycyclicRecognition.monoidModule_ascendingBase line 37