OAI/GroupTheory/PolycyclicRecognition/Geometry/NilpotentLieGroupNilpotent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Algebraic nilpotence of the simply connected nilpotent Lie models

The intrinsic height is zero when the tangent algebra is nilpotent. The constructed faithful representation is therefore upper unipotent on the whole group, and its finite matrix filtration proves group nilpotence.

  1. theorem OAI.PolycyclicRecognition.nilpotent_group_of_nilpotent_lieAlgebra line 19
  2. theorem OAI.PolycyclicRecognition.NilpotentLieModel.group_nilpotent line 47