OAI/GroupTheory/PolycyclicRecognition/Lattices/LatticeAutomorphismUnipotent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unipotence of a lattice automorphism induced by nilpotent conjugation

A polynomial surjective coordinate parameter suffices. Its integral grid only has to land in the lattice; no additive description of that lattice is assumed.

  1. theorem OAI.PolycyclicRecognition.lattice_automorphism_unipotent line 19