OAI/GroupTheory/SimpleAmenable/Homology/TranslationCoefficientAction.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RegularTranslation.C line 12
  2. lemma OAI.RegularTranslation.eqToHom_val line 13
  3. def OAI.RegularTranslation.shift line 14
  4. lemma OAI.RegularTranslation.shift_one line 19
  5. lemma OAI.RegularTranslation.shift_mul line 24
  6. def OAI.RegularTranslation.forward line 31
  7. lemma OAI.RegularCoefficient.comp_step line 38
  8. lemma OAI.RegularCoefficient.comp_pair line 44
  9. def OAI.RegularCoefficient.action line 53
  10. lemma OAI.RegularCoefficient.single_action line 55
  11. lemma OAI.RegularCoefficient.action_one line 60
  12. lemma OAI.RegularCoefficient.action_mul line 70
  13. def OAI.RegularCoefficient.representation line 82
  14. lemma OAI.ChainComplex.zeroπ_natural line 96
  15. lemma OAI.RegularCoefficient.zeroι_action line 103
  16. lemma OAI.RegularCoefficient.homology_action_zero line 110