SemisimpleLangTransversal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A global Lang transversal in the presence of fixed directions

The fixed-space projection and its complementary range preserve the lower central series. The map u,v ↦ u⁻¹ v A(u), written in these linear coordinates, is therefore a polynomial bijection even when A has fixed vectors.

theorem OAI.PolycyclicRecognition.semisimple_lang_transversal_bijective line 21
Source documentation
The global coordinate map for twisted conjugacy by a semisimple nilpotent-group automorphism. Its fixed component is retained explicitly.
```
theorem semisimple_lang_transversal_bijective (A : L ≃ₗ⁅ℝ⁆ L)
    (hA : Module.End.IsSemisimple A.toLinearMap) :
    let B : Module.End ℝ L := A.toLinearMap - 1
…
```