OAI/GroupTheory/PolycyclicRecognition/Geometry/CyclicJoinHeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The integer height on a subgroup generated over a normal kernel

  1. abbrev OAI.PolycyclicRecognition.cyclicJoin line 12
  2. abbrev OAI.PolycyclicRecognition.cyclicJoinLetter line 14
  3. abbrev OAI.PolycyclicRecognition.quotientLetter line 17
  4. theorem OAI.PolycyclicRecognition.quotientLetter_generates line 20
  5. def OAI.PolycyclicRecognition.cyclicJoinProjection line 26
  6. def OAI.PolycyclicRecognition.cyclicJoinHeight line 43
  7. theorem OAI.PolycyclicRecognition.cyclicJoinHeight_letter line 47
  8. theorem OAI.PolycyclicRecognition.cyclicJoinHeight_eq_one_iff line 51
  9. def OAI.PolycyclicRecognition.cyclicJoinHeightKernelEquiv line 66
  10. theorem OAI.PolycyclicRecognition.cyclicJoinHeightKernelEquiv_conj line 74