DiscreteNilpotentLieGroup.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Discrete subgroups of simply connected nilpotent Lie groups

Nilpotence makes every adjoint operator have only the zero generalized weight. A simultaneous triangular basis therefore has zero height, and the discrete height-kernel theorem applies to the whole group.

theorem OAI.PolycyclicRecognition.nonempty_triangularAdjoint_of_nilpotent line 21
Source documentation
Engel nilpotence supplies the split adjoint basis needed by the concrete height-kernel argument.
```
theorem nonempty_triangularAdjoint_of_nilpotent (L : Type*)
    [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L] [LieRing.IsNilpotent L] :
    ∃ n : ℕ, Nonempty (TriangularAdjoint L n) := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint
theorem OAI.PolycyclicRecognition.isPolycyclic_discrete_nilpotent_lieGroup line 40
Source documentation
Every discrete subgroup is polycyclic; finite generation is a conclusion.
```
theorem isPolycyclic_discrete_nilpotent_lieGroup
    [LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G)]
    (Γ : Subgroup G) [DiscreteTopology Γ] : IsPolycyclic Γ := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic