OAI/GroupTheory/PolycyclicRecognition/Analysis/IntegralSemisimpleTwist.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the actual semisimple generator action

The normalized section and its commuting semisimple factors are constructed in the original extension. Their integral action fixes the actual cocycle, and removing it leaves unipotent actions on every quotient generator.

  1. theorem OAI.PolycyclicRecognition.integral_semisimple_twist line 21