OAI/Algebra/GroupRing/WordCursor.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.WordCursor.value line 13
2. def OAI.TorsionFreeZeroDivisors.WordCursor.cursor line 14
3. lemma OAI.TorsionFreeZeroDivisors.WordCursor.value_nil line 15
4. lemma OAI.TorsionFreeZeroDivisors.WordCursor.value_cons line 16
5. lemma OAI.TorsionFreeZeroDivisors.WordCursor.value_append line 17
6. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_zero line 18
7. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_length line 19
8. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_succ line 20
9. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_append_left line 25
10. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_append_right line 29
11. lemma OAI.TorsionFreeZeroDivisors.WordCursor.cursor_cons_succ line 33
12. lemma OAI.TorsionFreeZeroDivisors.WordCursor.insert_old line 35
13. lemma OAI.TorsionFreeZeroDivisors.WordCursor.insert_first line 47
14. lemma OAI.TorsionFreeZeroDivisors.WordCursor.insert_second line 49
15. def OAI.TorsionFreeZeroDivisors.WordCursor.Paired line 52
16. lemma OAI.TorsionFreeZeroDivisors.WordCursor.inserted line 55
17. lemma OAI.TorsionFreeZeroDivisors.WordCursor.of_reduction line 92
18. lemma OAI.TorsionFreeZeroDivisors.WordCursor.of_identity line 104