SemisimpleCocycleReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Eliminating a moving central component of an extension cocycle

This constructs the projected factor system and an actual kernel correction. The corrected factors are fixed by S; no splitting of the original extension or existence of a cocycle correction is assumed.

theorem OAI.PolycyclicRecognition.semisimple_cocycle_reduction line 21