OAI/GroupTheory/PolycyclicRecognition/Geometry/TangentRotationRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact rotations on the concrete model space of a Lie group

  1. def OAI.PolycyclicRecognition.tangentTorusUnitAction line 17

    Source documentation

    This version uses the original model-space norm and scalar structures.

    def tangentTorusUnitAction :
    realRotationTorus (GroupLieAlgebra (𝓘(ℝ,E)) G) H →* (E →L[ℝ] E)ˣ where
…

    Mentions: OAI.PolycyclicRecognition.realRotationTorus

  2. theorem OAI.PolycyclicRecognition.continuous_tangentTorusUnitAction line 33
  3. theorem OAI.PolycyclicRecognition.contMDiff_tangentTorusRepresentation line 50