OAI/GroupTheory/PolycyclicRecognition/Geometry/DerivationFlowRepresentation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Representing a nilpotent derivation flow by conjugation

Only the given intertwining identity is used. The target operator need not be nilpotent outside the image of the intertwiner.

  1. theorem OAI.PolycyclicRecognition.nilpotentDerivationFlow_eq_analytic line 23
  2. theorem OAI.PolycyclicRecognition.derivationFlow_representation line 43
  3. theorem OAI.PolycyclicRecognition.derivationFlow_group_conjugation line 59