OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeDerivationLog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The cyclic lattice step from an actual derivation logarithm

The logarithm and its exponential equality remain a local algebraic obligation. The real action and the Lie lattice are constructed here.

  1. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.cyclic_lattice_of_derivation_log line 18
  2. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.cyclic_finiteIndex_lattice_of_derivation_log line 35