OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentLieExistenceConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent model existence by dimension induction

Only the published finite BCH formula on already constructed, smaller models is used. No general Lie existence or integration theorem is assumed.

  1. theorem OAI.PolycyclicRecognition.nilpotentLieModel_of_dynkin line 22
  2. theorem OAI.PolycyclicRecognition.nilpotentLieExistenceInput_of_dynkin line 47