OAI/GroupTheory/PolycyclicRecognition/Lattices/RealActionIntegerLattice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Time-one invariance constructs a lattice in a real semidirect product

  1. theorem OAI.PolycyclicRecognition.subgroup_mem_mulAut_zpow line 13
  2. theorem OAI.PolycyclicRecognition.realAction_integerLattice_preserves line 32
  3. theorem OAI.PolycyclicRecognition.realAction_integerLattice_uniform line 48