OAI/GroupTheory/PolycyclicRecognition/Geometry/InvariantGraphLieModel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The analytic solvable model on an invariant graph

The graph uses the original vector-space chart. Its operations are analytic, and its dimension is the dimension of the nilpotent group alone.

  1. def OAI.PolycyclicRecognition.invariantGraphEquiv line 25
  2. def OAI.PolycyclicRecognition.invariantGraphGroup line 36
  3. theorem OAI.PolycyclicRecognition.invariantGraphLieGroup line 40
  4. def OAI.PolycyclicRecognition.invariantGraphMulEquiv line 64
  5. def OAI.PolycyclicRecognition.invariantGraphLieModel line 77
  6. def OAI.PolycyclicRecognition.invariantGraphModelEquiv line 97
  7. theorem OAI.PolycyclicRecognition.invariantGraphModelEquiv_continuous line 102
  8. theorem OAI.PolycyclicRecognition.invariantGraphModelEquiv_symm_continuous line 106