TriangulableLatticePolycyclic.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Polycyclicity of lattices in the actual triangulable model

Finite generation comes from compactness and metric chains. The real triangular adjoint representation then identifies a polycyclic kernel and abelian height quotient. No lattice structure theorem is assumed for this specialization.

theorem OAI.PolycyclicRecognition.isPolycyclic_uniformLattice_of_realTriangulable line 22
Source documentation
The uniform-lattice polycyclicity theorem for a real-triangulable, connected simply connected solvable Lie model.
```
theorem isPolycyclic_uniformLattice_of_realTriangulable
    (S : SimplyConnectedSolvableLieModel) (hS : IsRealTriangulable S)
    (Λ : Subgroup S.carrier) (hΛ : IsUniformLattice Λ) : IsPolycyclic Λ := by
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsRealTriangulable, OAI.PolycyclicRecognition.IsPolycyclic