OAI/GroupTheory/PolycyclicRecognition/Lattices/SemisimpleLangDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Inner perturbations of a semisimple nilpotent automorphism

The fixed part of the Lang transversal is retained. It commutes with the semisimple automorphism, while the moving part is absorbed by conjugation.

  1. theorem OAI.PolycyclicRecognition.semisimple_lang_decomposition line 17
  2. theorem OAI.PolycyclicRecognition.semisimple_inner_twist line 31