OAI/GroupTheory/PolycyclicRecognition/Algebra/AlgebraOneParameter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiable one-parameter subgroups in a real Banach algebra

The derivative at zero determines the curve. Multiplication by the inverse exponential produces a function with zero derivative everywhere.

  1. theorem OAI.PolycyclicRecognition.oneParameter_hasDerivAt line 19
  2. theorem OAI.PolycyclicRecognition.oneParameter_eq_exp line 34