OAI/GroupTheory/PolycyclicRecognition/Lattices/AbelianCyclicLogarithmLattice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The abelian cyclic lattice step from a real matrix logarithm

The real logarithm is a separate, explicit linear algebra obligation. Once it is provided, the actual Lie model and compact lattice cover are constructed.

  1. theorem OAI.PolycyclicRecognition.freeAbelian_cyclic_lattice_of_linear_log line 17