OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicTriangularRealization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete triangular realization without a global exponential chart

  1. theorem OAI.PolycyclicRecognition.onshuusPostRealizationInput_intrinsic line 18
  2. theorem OAI.PolycyclicRecognition.exponentialLinearRealizationInput_intrinsic line 48

    Source documentation

    The exponential-compatible inducing linear realization is constructed from the actual Lie group, with no published realization premise.

    theorem exponentialLinearRealizationInput_intrinsic :
    ExponentialLinearRealizationInput (EG := E) (G := G) := by
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput