OAI/GroupTheory/PolycyclicRecognition/Algebra/SemisimpleInnerFixedRepresentative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed representatives of inner automorphisms centralizing a semisimple map

An element whose inner action centralizes S differs, by a central element, from an S-fixed element. The representative is the canonical linear fixed projection, so it preserves all invariant subspaces as well.

  1. theorem OAI.PolycyclicRecognition.semisimple_inner_fixed_representative_preserves line 20
  2. theorem OAI.PolycyclicRecognition.semisimple_inner_fixed_representative line 77