OAI/GroupTheory/PolycyclicRecognition/Lattices/AbelianCyclicFiniteIndexLattice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Free-abelian-by-cyclic groups are virtually solvable Lie lattices

No nilpotence assumption is required. Squaring the integral automorphism permits a real logarithm, and its exponential supplies the real action.

  1. theorem OAI.PolycyclicRecognition.realIntegralLinearEquiv_square line 16
  2. theorem OAI.PolycyclicRecognition.freeAbelian_cyclic_finiteIndex_lattice line 29