OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteCentralizerCommutator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The centralizer of a finite-index subgroup has finite commutator

  1. theorem OAI.PolycyclicRecognition.commutatorElement_center_mul_left line 12
  2. theorem OAI.PolycyclicRecognition.commutatorElement_center_mul_right line 19
  3. theorem OAI.PolycyclicRecognition.commutator_finite_of_center_finiteIndex line 26
  4. theorem OAI.PolycyclicRecognition.centralizer_commutator_finite line 51