OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentAlgebraRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating nilpotent factor representations into matrix units

The source model is arbitrary and the represented matrices need not be nilpotent. Only the source Lie algebra is nilpotent.

  1. theorem OAI.PolycyclicRecognition.NilpotentLieModel.exists_algebra_representation line 18