OAI/Algebra/GroupRing/IndexedCells.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.in_range line 17
2. def OAI.TorsionFreeZeroDivisors.IndexedCells.loop line 19
3. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.loop_equal line 21
4. def OAI.TorsionFreeZeroDivisors.IndexedCells.attaching line 23
5. abbrev OAI.TorsionFreeZeroDivisors.IndexedCells.Cover line 24
6. abbrev OAI.TorsionFreeZeroDivisors.IndexedCells.Base line 25
7. def OAI.TorsionFreeZeroDivisors.IndexedCells.inclusion line 26
8. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.mapped_loop line 27
9. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.wordLift_rel line 35
10. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.cover_simplyConnected line 47
11. def OAI.TorsionFreeZeroDivisors.IndexedCells.translated line 50
12. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.translated_equal line 54
13. lemma OAI.TorsionFreeZeroDivisors.IndexedCells.attaching_translated line 57