OAI/GroupTheory/PolycyclicRecognition/Finiteness/OrientationHomologyAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Ambient conjugation on the local top orientation homology

  1. theorem OAI.PolycyclicRecognition.orientation_action_invariant line 17
  2. def OAI.PolycyclicRecognition.invariantConjugationCoefficient line 34
  3. def OAI.PolycyclicRecognition.invariantConjugationHomologyMap line 42
  4. theorem OAI.PolycyclicRecognition.invariantConjugationHomologyMap_one line 48
  5. theorem OAI.PolycyclicRecognition.invariantConjugationHomologyMap_mul line 57
  6. def OAI.PolycyclicRecognition.invariantConjugationHomologyAction line 70