OAI/GroupTheory/PolycyclicRecognition/Lattices/LatticeWordExtension.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extending lattice automorphisms through ordered polynomial coordinates

The extension is constructed by replacing each integral generator power by the corresponding real one-parameter subgroup. Polynomial identities prove both multiplicativity and the inverse identities.

  1. def OAI.PolycyclicRecognition.latticeWordMap line 21
  2. theorem OAI.PolycyclicRecognition.latticeWordMap_polynomial line 24
  3. theorem OAI.PolycyclicRecognition.latticeWordMap_on_lattice line 28
  4. def OAI.PolycyclicRecognition.latticeWordAut line 40
  5. theorem OAI.PolycyclicRecognition.latticeWordAut_on_lattice line 69
  6. theorem OAI.PolycyclicRecognition.contMDiff_latticeWordAut line 77