OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacteristicCyclicSubgroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restricting a cyclic extension to a characteristic finite-index base

  1. def OAI.PolycyclicRecognition.characteristicCyclicMap line 12
  2. theorem OAI.PolycyclicRecognition.characteristicCyclicMap_injective line 22
  3. theorem OAI.PolycyclicRecognition.mem_characteristicCyclicMap_range line 29
  4. theorem OAI.PolycyclicRecognition.characteristicCyclicMap_finiteIndex line 37