OAI/GroupTheory/PolycyclicRecognition/Algebra/SemisimpleInnerCentralizer.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The kernel of a semisimple action centralizer

An inner automorphism centralizes a semisimple S exactly when its defining element is a product of a central element and an S-fixed element.

  1. theorem OAI.PolycyclicRecognition.central_quotient_of_inner_eq line 18
  2. theorem OAI.PolycyclicRecognition.semisimple_inner_centralizer_decomposition line 36
  3. theorem OAI.PolycyclicRecognition.semisimple_inner_centralizer_iff line 43