OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicExponentialSmooth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Smoothness of the intrinsic real triangular exponential

The inducing representation first proves continuity. Smooth cancellation then recovers the actual manifold regularity from the matrix exponential. No global exponential chart is used.

  1. theorem OAI.PolycyclicRecognition.intrinsic_exponential_contMDiff line 24