OAI/Algebra/GroupRing/WordFrames.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.WordFrames.words line 14
2. def OAI.TorsionFreeZeroDivisors.WordFrames.position line 15
3. structure OAI.TorsionFreeZeroDivisors.WordFrames.Data line 19
4. def OAI.TorsionFreeZeroDivisors.WordFrames.Data.rename line 24
5. def OAI.TorsionFreeZeroDivisors.WordFrames.Data.removeCaps line 35
6. def OAI.TorsionFreeZeroDivisors.WordFrames.focus line 47
7. lemma OAI.TorsionFreeZeroDivisors.WordFrames.focus_letter line 52
8. lemma OAI.TorsionFreeZeroDivisors.WordFrames.focus_rotation line 66
9. lemma OAI.TorsionFreeZeroDivisors.WordFrames.focus_position line 82
10. def OAI.TorsionFreeZeroDivisors.WordFrames.Data.focus line 100
11. def OAI.TorsionFreeZeroDivisors.WordFrames.Data.unfocus line 104