OAI/GroupTheory/PolycyclicRecognition/Algebra/UnconditionalNilpotentModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Simply connected nilpotent model existence without published inputs

  1. def OAI.PolycyclicRecognition.polynomialCoordinateLieModel line 12
  2. theorem OAI.PolycyclicRecognition.nilpotentLieModel_exists line 18
  3. theorem OAI.PolycyclicRecognition.nilpotentLieExistenceInput line 24