LieExponential.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential maps of actual real Lie groups

The differential and one-parameter-subgroup characterization identifies the ordinary Lie-group exponential without requiring a pre-existing library construction of its global flow.

structure OAI.PolycyclicRecognition.IsGroupExponential line 26
Source documentation
The intrinsic exponential, characterized by its one-parameter subgroups and their tangent vectors at the identity. The Lie algebra here is the actual tangent Lie algebra of G, with its invariant-vector-field bracket.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:181 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.IsGroupExponential@path.
```
structure IsGroupExponential (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) : Prop where
…
```
theorem OAI.PolycyclicRecognition.IsGroupExponential.map_neg line 35