OAI/GroupTheory/PolycyclicRecognition/Geometry/InnerTwistJordanFactor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Semisimple factors in an inner coset

Changing a nilpotent-group automorphism by inner conjugation changes its semisimple Jordan factor by inner conjugation. The conjugating element is constructed by the global Lang transversal.

  1. theorem OAI.PolycyclicRecognition.inner_normal_form_semisimple_factor line 19
  2. theorem OAI.PolycyclicRecognition.inner_twist_semisimple_factor line 55