OAI/Algebra/GroupRing/LoopTranspose.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.LoopTranspose.Other line 14
2. instance OAI.TorsionFreeZeroDivisors.LoopTranspose.(instance at line 15) line 15
3. def OAI.TorsionFreeZeroDivisors.LoopTranspose.groupEquiv line 19
4. def OAI.TorsionFreeZeroDivisors.LoopTranspose.equiv line 27
5. def OAI.TorsionFreeZeroDivisors.LoopTranspose.turnPath line 33
6. lemma OAI.TorsionFreeZeroDivisors.LoopTranspose.turnPath_turn line 43
7. def OAI.TorsionFreeZeroDivisors.LoopTranspose.turn line 46
8. lemma OAI.TorsionFreeZeroDivisors.LoopTranspose.equiv_mk line 49
9. lemma OAI.TorsionFreeZeroDivisors.LoopTranspose.turn_equiv_mk line 54
10. lemma OAI.TorsionFreeZeroDivisors.LoopTranspose.turns_representative line 58
11. lemma OAI.TorsionFreeZeroDivisors.LoopTranspose.turn_mk line 69