OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectCoordinateOrbit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial coordinate orbits in the nilpotent semidirect construction

  1. def OAI.PolycyclicRecognition.semidirectCoordinate line 21
  2. theorem OAI.PolycyclicRecognition.semidirectCoordinate_injective line 26
  3. theorem OAI.PolycyclicRecognition.contDiff_semidirectCoordinate line 36
  4. def OAI.PolycyclicRecognition.semidirectFlowCoordinatePolynomial line 42
  5. theorem OAI.PolycyclicRecognition.semidirectFlowCoordinatePolynomial_eval line 49
  6. def OAI.PolycyclicRecognition.semidirectProductCoordinatePolynomial line 64
  7. theorem OAI.PolycyclicRecognition.semidirectProductCoordinatePolynomial_eval line 70
  8. theorem OAI.PolycyclicRecognition.finiteDimensional_semidirectCoordinateOrbit line 91