OAI/GroupTheory/PolycyclicRecognition/Algebra/AlgebraTangentSolvable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Solvability of the infinitesimal action of a solvable matrix group

The group derived series controls successive commutators of the tangent spans. This avoids assuming a closed-subgroup or Lie–Kolchin theorem.

  1. theorem OAI.PolycyclicRecognition.algebraGroupTangentLie_isSolvable line 21

    Source documentation

    The tangent Lie algebra of a solvable subgroup of units is solvable.

    theorem algebraGroupTangentLie_isSolvable (D : Subgroup Aˣ) [Group.IsSolvable D] :
    LieAlgebra.IsSolvable (algebraGroupTangentLie D) := by
…

    Mentions: OAI.PolycyclicRecognition.algebraGroupTangentLie