OAI/GroupTheory/PolycyclicRecognition/Algebra/SemisimpleCentralizerExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact extension carried by a semisimple centralizer

  1. theorem OAI.PolycyclicRecognition.inl_mem_semisimpleCentralizer_iff line 15
  2. def OAI.PolycyclicRecognition.semisimpleCentralizerInclusion line 38
  3. def OAI.PolycyclicRecognition.semisimpleCentralizerExtension line 44
  4. theorem OAI.PolycyclicRecognition.semisimpleCentralizerExtension_conjAct line 67