OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteSemisimpleCocycleReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing all moving components for a finite semisimple family

Each correction is central and fixes every component already dealt with. Their product is one normalized gauge for the original factor system.

  1. theorem OAI.PolycyclicRecognition.finite_semisimple_cocycle_reduction line 20