OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteSemisimpleLiftFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite commuting semisimple family adapted to quotient generators

Successive inner corrections preserve the earlier semisimple factors. Every member of a finite list in the abelian quotient therefore has a lift in one common centralizer, with its semisimple factor belonging to that family.

  1. theorem OAI.PolycyclicRecognition.extension_conjugationLinear_inl_mul line 21
  2. def OAI.PolycyclicRecognition.HasSemisimpleLift line 34
  3. theorem OAI.PolycyclicRecognition.HasSemisimpleLift.extend line 43
  4. theorem OAI.PolycyclicRecognition.exists_finite_semisimple_lift_family line 61