OAI/GroupTheory/PolycyclicRecognition/Geometry/SemisimpleLieLogarithm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite power of a semisimple Lie automorphism has a derivation logarithm

The logarithm uses one additive character on the generated spectral group, so the derivative respects every bracket relation.

  1. class OAI.PolycyclicRecognition.ComplexNormedLieAlgebra line 16

    Source documentation

    The analytic and Lie structures share their additive and scalar data.

    class ComplexNormedLieAlgebra (L : Type*) extends NormedAddCommGroup L, LieRing L,
    NormedSpace ℂ L, LieAlgebra ℂ L

variable {L : Type} [ComplexNormedLieAlgebra L] [FiniteDimensional ℂ L] [CompleteSpace L]
  2. theorem OAI.PolycyclicRecognition.semisimple_lie_automorphism_has_power_log line 21
  3. theorem OAI.PolycyclicRecognition.semisimple_real_form_has_commuting_power_log line 31
  4. theorem OAI.PolycyclicRecognition.semisimple_real_form_has_power_log line 46