CartanRealShadowSolvable.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PolycyclicRecognition.realShadowKernel line 17
Source documentation
The same weight kernel, now inside the modified Lie algebra.
```
def realShadowKernel : LieIdeal ℝ (CartanRealShadow T H) where
…
```
Mentions: OAI.PolycyclicRecognition.CartanRealShadow
def OAI.PolycyclicRecognition.realShadowKernelEquiv line 27
Source documentation
On the nilpotent ideal the modified and original brackets agree.
```
def realShadowKernelEquiv : T.kernelIdeal ≃ₗ⁅ℝ⁆ realShadowKernel T H where
…
```
Mentions: OAI.PolycyclicRecognition.realShadowKernel
theorem OAI.PolycyclicRecognition.realShadowKernel_nilpotent line 53
theorem OAI.PolycyclicRecognition.cartanRealShadow_solvable line 58
Source documentation
The real shadow is solvable because its derived algebra lies in the unchanged nilpotent weight kernel.
```
theorem cartanRealShadow_solvable : LieAlgebra.IsSolvable (CartanRealShadow T H) := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanRealShadow