OAI/GroupTheory/PolycyclicRecognition/Geometry/CharacteristicSemidirectSubgroup.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A characteristic finite-index base in a semidirect product

  1. def OAI.PolycyclicRecognition.characteristicSemidirectMap line 12
  2. theorem OAI.PolycyclicRecognition.characteristicSemidirectMap_injective line 16
  3. theorem OAI.PolycyclicRecognition.mem_characteristicSemidirectMap_range line 24
  4. theorem OAI.PolycyclicRecognition.characteristicSemidirectMap_finiteIndex line 32