OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeInduction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Realizing an arbitrary finitely generated torsion-free nilpotent group

The induction follows an actual torsion-free cyclic series. Its successive integer normal forms are retained as polynomial parameters at every stage.

  1. theorem OAI.PolycyclicRecognition.nilpotent_lattice_coordinates_of_cyclic_quotient line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_lattice_coordinates_of_polyZ line 53
  3. theorem OAI.PolycyclicRecognition.nilpotent_lattice_coordinates line 76
  4. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.solvableLieModel line 82
  5. theorem OAI.PolycyclicRecognition.torsionFree_nilpotent_uniform_lattice line 86