OAI/GroupTheory/PolycyclicRecognition/Algebra/CommonSemisimpleCentralizer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Common semisimple centralizers in the completed extension

  1. def OAI.PolycyclicRecognition.commonSemisimpleCentralizer line 15
  2. theorem OAI.PolycyclicRecognition.mem_commonSemisimpleCentralizer line 19
  3. theorem OAI.PolycyclicRecognition.inl_mem_commonSemisimpleCentralizer_of_fixed line 26
  4. theorem OAI.PolycyclicRecognition.mem_semisimpleActionCentralizer_iff line 44
  5. theorem OAI.PolycyclicRecognition.common_semisimpleCentralizer_step line 70