OAI/GroupTheory/PolycyclicRecognition/Algebra/SubgroupInductionCoordinates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Direct-sum coordinates for induction from an arbitrary subgroup

Right cosets, with a chosen representative, are sufficient. No normality of the subgroup is required for exact induction or for the rational base case.

  1. abbrev OAI.PolycyclicRecognition.subgroupRightCosets line 18
  2. def OAI.PolycyclicRecognition.subgroupRightCoset line 19
  3. def OAI.PolycyclicRecognition.subgroupRightRepresentative line 20
  4. theorem OAI.PolycyclicRecognition.subgroupRightRepresentative_coset line 23
  5. theorem OAI.PolycyclicRecognition.subgroupRightCoset_mul line 27
  6. def OAI.PolycyclicRecognition.subgroupRightPart line 32
  7. theorem OAI.PolycyclicRecognition.subgroupRightPart_decompose line 38
  8. theorem OAI.PolycyclicRecognition.subgroupRightPart_mul line 43
  9. theorem OAI.PolycyclicRecognition.subgroupRightPart_representative line 49
  10. def OAI.PolycyclicRecognition.subgroupInductionTensorCoordinates line 56
  11. theorem OAI.PolycyclicRecognition.subgroupInductionTensorCoordinates_single line 64
  12. theorem OAI.PolycyclicRecognition.subgroupInductionTensorCoordinates_invariant line 69
  13. def OAI.PolycyclicRecognition.subgroupInductionCoordinates line 81
  14. theorem OAI.PolycyclicRecognition.subgroupInductionCoordinates_mk line 86
  15. def OAI.PolycyclicRecognition.subgroupInductionCoordinatesInv line 91
  16. theorem OAI.PolycyclicRecognition.subgroupInductionCoordinatesInv_single line 95
  17. theorem OAI.PolycyclicRecognition.subgroupInductionCoordinates_right_inv line 100
  18. theorem OAI.PolycyclicRecognition.subgroupInductionCoordinates_left_inv line 113
  19. def OAI.PolycyclicRecognition.subgroupInductionEquiv line 132