OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialAutomorphismTopology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Topology of the integrated nilpotent automorphisms

  1. theorem OAI.PolycyclicRecognition.continuous_exponentialConjugate line 23
  2. def OAI.PolycyclicRecognition.integrateNilpotentLieEquivContinuous line 41

    Source documentation

    Both directions of exponential conjugation are continuous, and the published finite Dynkin formula proves its multiplicativity.

    def integrateNilpotentLieEquivContinuous
    (dynkin : NilpotentDynkinExpansionInput E G) (hExp : IsGroupExponential Exp)
    {c : ℕ} (hc : lowerCentralSeries ℝ L L c = ⊥) (F : L ≃ₗ⁅ℝ⁆ L) : G ≃ₜ* G := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput