OAI/GroupTheory/PolycyclicRecognition/Geometry/JordanInnerTwist.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Jordan normal form after an arbitrary inner perturbation

The global Lang transversal moves the perturbing element into the fixed subgroup of the semisimple factor. Its remaining inner action combines with the unipotent factor without losing unipotence.

  1. theorem OAI.PolycyclicRecognition.jordan_inner_twist_normal_form line 20
  2. theorem OAI.PolycyclicRecognition.inner_twist_has_original_semisimple_normal_form line 57