OAI/GroupTheory/PolycyclicRecognition/Algebra/InnerCentralizerFactorSystem.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Restriction of a factor system to the inner centralizer

Commutation of every quotient action with S forces every section factor into the inner centralizer. The restriction retains the exact nonabelian cocycle.

  1. theorem OAI.PolycyclicRecognition.factor_mem_innerCentralizer line 19
  2. def OAI.PolycyclicRecognition.innerCentralizerFactorSystem line 35