OAI/GroupTheory/PolycyclicRecognition/Algebra/RegularDualFree.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The regular dual of a finite free group-ring module

  1. def OAI.PolycyclicRecognition.regularInversion line 18
  2. theorem OAI.PolycyclicRecognition.regularInversion_single line 21
  3. theorem OAI.PolycyclicRecognition.regularInversion_rightTranslation line 25
  4. def OAI.PolycyclicRecognition.regularDualFreeEquiv line 36
  5. theorem OAI.PolycyclicRecognition.regularDualFreeEquiv_apply line 42
  6. def OAI.PolycyclicRecognition.regularDualFreeIso line 47
  7. theorem OAI.PolycyclicRecognition.regularDualFreeIso_inv_single line 69