AlgebraTangentLie.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The Lie algebra of tangent spans

Bilinearity extends the computed commutator identity from curve derivatives to their finite linear span. Thus the derived group controls the derived Lie algebra without a closed-subgroup theorem.

theorem OAI.PolycyclicRecognition.algebraGroupTangentSpan_commutator line 22
Source documentation
Commutators of tangent spans lie in the tangent span of the derived group.
```
theorem algebraGroupTangentSpan_commutator {D : Subgroup Aˣ} {X Y : A}
    (hX : X ∈ algebraGroupTangentSpan D) (hY : Y ∈ algebraGroupTangentSpan D) :
    X * Y - Y * X ∈ algebraGroupTangentSpan ⁅D, D⁆ := by
…
```
Mentions: OAI.PolycyclicRecognition.algebraGroupTangentSpan
def OAI.PolycyclicRecognition.algebraGroupTangentLie line 45
Source documentation
The tangent span is a concrete Lie subalgebra of the ambient matrix algebra.
```
def algebraGroupTangentLie (D : Subgroup Aˣ) : LieSubalgebra ℝ A :=
…
```