OAI/GroupTheory/PolycyclicRecognition/Algebra/RegularPairingNaturality.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Naturality of the regular-dual evaluation pairing

  1. theorem OAI.PolycyclicRecognition.regularDualMap_id line 17
  2. theorem OAI.PolycyclicRecognition.regularDualMap_comp line 24
  3. theorem OAI.PolycyclicRecognition.regularCoinvariantEvaluation_naturality line 31