OAI/GroupTheory/PolycyclicRecognition/Geometry/RealPhaseExponential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact Cartan rotations as exponentials of their imaginary derivations

  1. def OAI.PolycyclicRecognition.tangentImaginaryOperator line 19

    Source documentation

    The imaginary derivation with the original model-space norm.

    def tangentImaginaryOperator (h : H) : E →L[ℝ] E :=
…
  2. theorem OAI.PolycyclicRecognition.tangentPhase_eq_exp line 22
  3. theorem OAI.PolycyclicRecognition.tangentPhase_inv_eq_exp line 53