OAI/GroupTheory/PolycyclicRecognition/Geometry/FixedVectorLieLogarithm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The chosen Lie logarithm vanishes on fixed vectors

The compatible spectral character has value zero at the identity. This retains the quotient directions when extending the integral nilshadow action.

  1. theorem OAI.PolycyclicRecognition.spectralLogValue_one line 20
  2. theorem OAI.PolycyclicRecognition.spectralLieDerivation_fixed line 26
  3. theorem OAI.PolycyclicRecognition.semisimple_real_form_has_fixed_power_log line 37
  4. theorem OAI.PolycyclicRecognition.real_semisimple_has_fixed_power_log line 58
  5. theorem OAI.PolycyclicRecognition.lie_jordan_fixed line 98
  6. theorem OAI.PolycyclicRecognition.unipotentLieLogarithm_fixed line 126