OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianCyclicSquareLog.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A logarithm of the squared automorphism suffices for the lattice

The square gives a concrete finite-index subgroup. Thus the matrix logarithm needed for the real action may be taken after this finite-index passage.

  1. theorem OAI.PolycyclicRecognition.freeAbelian_cyclic_finiteIndex_lattice_of_square_log line 16