OAI/Algebra/GroupRing/CellModule.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TorsionFreeZeroDivisors.CellModule.Module line 12
  2. def OAI.TorsionFreeZeroDivisors.CellModule.translate line 13
  3. lemma OAI.TorsionFreeZeroDivisors.CellModule.translate_apply line 15
  4. lemma OAI.TorsionFreeZeroDivisors.CellModule.translate_single line 17
  5. lemma OAI.TorsionFreeZeroDivisors.CellModule.translate_one line 22
  6. lemma OAI.TorsionFreeZeroDivisors.CellModule.translate_mul line 23
  7. def OAI.TorsionFreeZeroDivisors.CellModule.action line 25
  8. abbrev OAI.TorsionFreeZeroDivisors.CellModule.Crossed line 30
  9. def OAI.TorsionFreeZeroDivisors.CellModule.lift line 31
  10. lemma OAI.TorsionFreeZeroDivisors.CellModule.lift_right line 33
  11. def OAI.TorsionFreeZeroDivisors.CellModule.fox line 37
  12. lemma OAI.TorsionFreeZeroDivisors.CellModule.fox_one line 38
  13. lemma OAI.TorsionFreeZeroDivisors.CellModule.fox_of line 39
  14. lemma OAI.TorsionFreeZeroDivisors.CellModule.fox_mul line 41
  15. lemma OAI.TorsionFreeZeroDivisors.CellModule.fox_inv line 44
  16. def OAI.TorsionFreeZeroDivisors.CellModule.boundary line 51
  17. lemma OAI.TorsionFreeZeroDivisors.CellModule.boundary_single line 55
  18. lemma OAI.TorsionFreeZeroDivisors.CellModule.boundary_translate line 59
  19. lemma OAI.TorsionFreeZeroDivisors.CellModule.boundary_fox line 65