OAI/GroupTheory/PolycyclicRecognition/Lattices/FiniteFixedCocycleSection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneously fixed section factors for finitely many quotient lifts

The original extension has a normalized section centralizing a finite commuting semisimple family. All its factors are fixed by that entire family, and the specified quotient elements retain their semisimple Jordan factors.

  1. theorem OAI.PolycyclicRecognition.inl_mem_semisimpleCentralizer_of_center line 22
  2. theorem OAI.PolycyclicRecognition.exists_finite_fixed_cocycle_section line 36