SolvableGroupLieAlgebra.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The Lie algebra of an actual solvable Lie group

The intrinsic adjoint exponential puts the adjoint representation into the infinitesimal action of a solvable matrix group. Its derived series vanishes; one additional bracket kills the central kernel of the adjoint action.

theorem OAI.PolycyclicRecognition.groupLieAlgebra_isSolvable line 24
Source documentation
Group solvability implies solvability of the intrinsic tangent Lie algebra.
```
theorem groupLieAlgebra_isSolvable :
    LieAlgebra.IsSolvable (GroupLieAlgebra (𝓘(ℝ, E)) G) := by
…
```