OAI/GroupTheory/PolycyclicRecognition/Geometry/RealLieAutomorphismPowerLog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite power of every real Lie automorphism has a derivation logarithm

The semisimple logarithm respects spectral multiplicative relations and the real form. Its commutation with the unipotent logarithm allows the two flows to be combined.

  1. theorem OAI.PolycyclicRecognition.real_lie_automorphism_has_commuting_power_log line 21
  2. theorem OAI.PolycyclicRecognition.real_lie_automorphism_has_power_log line 60