OAI/GroupTheory/PolycyclicRecognition/Geometry/RepresentationFromDifferential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential compatibility of triangular realizations

The matrix derivative determines each one-parameter subgroup. An inducing realization and its matrix differential therefore give exponential-linear compatibility.

  1. theorem OAI.PolycyclicRecognition.matrixLieDifferential_exponential line 21
  2. theorem OAI.PolycyclicRecognition.exponentialLinearRealizationInput_of_triangular line 37