OAI/GroupTheory/PolycyclicRecognition/Algebra/InducedTranslation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The chain-level translation associated to a lift of a quotient generator

  1. theorem OAI.PolycyclicRecognition.inductionMap_comp_semilinear line 17
  2. theorem OAI.PolycyclicRecognition.semilinear_comp_inductionMap line 33
  3. def OAI.PolycyclicRecognition.conjugatedResolution line 52
  4. def OAI.PolycyclicRecognition.conjugationResolutionLift line 59
  5. def OAI.PolycyclicRecognition.inducedTranslation line 63