OAI/GroupTheory/PolycyclicRecognition/Algebra/NormalQuotientCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Coset coordinates for induction from a normal subgroup

  1. def OAI.PolycyclicRecognition.normalQuotientRepresentative line 12
  2. theorem OAI.PolycyclicRecognition.normalQuotientRepresentative_mk line 15
  3. theorem OAI.PolycyclicRecognition.normalQuotient_mk_subgroup line 19
  4. def OAI.PolycyclicRecognition.normalQuotientPart line 23
  5. theorem OAI.PolycyclicRecognition.normalQuotientPart_mul line 30
  6. theorem OAI.PolycyclicRecognition.normalQuotientPart_representative line 38
  7. theorem OAI.PolycyclicRecognition.normalQuotientPart_decompose line 46