OAI/GroupTheory/PolycyclicRecognition/Analysis/OneParameterIntegralCurve.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering a one-parameter subgroup from its tangent vector

  1. theorem OAI.PolycyclicRecognition.oneParameter_isMIntegralCurve line 16
  2. theorem OAI.PolycyclicRecognition.oneParameter_eq_groupExponential line 52