SplitLieQuotient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Split Lie actions pass to invariant quotients

The simultaneous-basis form of Lie's theorem requires induction on a quotient by a common eigenline. We prove the splitting hypothesis for that quotient using images of the original generalized eigenspaces.

theorem OAI.PolycyclicRecognition.quotient_isTriangularizable line 26
Source documentation
A quotient of a split Lie action remains split. The image of each generalized eigenspace lies in the corresponding quotient eigenspace.
```
theorem quotient_isTriangularizable [LieModule.IsTriangularizable 𝕜 L V]
    (N : LieSubmodule 𝕜 L V) : LieModule.IsTriangularizable 𝕜 L (V ⧸ N) := by
…
```