OAI/RingTheory/DirectFiniteness/AssignedDevelopment.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.AssignedDirections.incidenceMap line 14
2. lemma OAI.KaplanskyCounterexample.AssignedDirections.incidenceMap_injective line 17
3. lemma OAI.KaplanskyCounterexample.AssignedDirections.incidenceMap_independent line 20
4. lemma OAI.KaplanskyCounterexample.AssignedDirections.incidenceMap_covers line 24
5. abbrev OAI.KaplanskyCounterexample.AssignedDevelopment.maps line 38
6. lemma OAI.KaplanskyCounterexample.AssignedDevelopment.covers line 40
7. abbrev OAI.KaplanskyCounterexample.AssignedDevelopment.Base line 43
8. def OAI.KaplanskyCounterexample.AssignedDevelopment.point line 45
9. lemma OAI.KaplanskyCounterexample.AssignedDevelopment.point_injective line 49
10. def OAI.KaplanskyCounterexample.AssignedDevelopment.line line 61
11. lemma OAI.KaplanskyCounterexample.AssignedDevelopment.point_direction line 66
12. lemma OAI.KaplanskyCounterexample.AssignedDevelopment.line_injective line 75
13. lemma OAI.KaplanskyCounterexample.AssignedDevelopment.subgroup_decomposition line 83