OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialKernelCentral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Periods of the real triangular exponential are central

This reduces possible failure of injectivity to the central directions, without a global exponential chart or a faithful group representation.

  1. theorem OAI.PolycyclicRecognition.lie_bracket_zero_of_exponential_eq_one line 21