OAI/RingTheory/DirectFiniteness/CycleSums.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.Planar.sumCongr_sameCycle_inl line 15
2. lemma OAI.KaplanskyCounterexample.Planar.sumCongr_sameCycle_inr line 21
3. lemma OAI.KaplanskyCounterexample.Planar.sumCongr_not_sameCycle line 27
4. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_sum_left line 33
5. lemma OAI.KaplanskyCounterexample.Planar.sum_cycle_sum_right line 55
6. def OAI.KaplanskyCounterexample.Planar.cycleInl line 77
7. lemma OAI.KaplanskyCounterexample.Planar.cycleInl_class line 80
8. lemma OAI.KaplanskyCounterexample.Planar.cycleInl_injective line 83
9. lemma OAI.KaplanskyCounterexample.Planar.cycleInl_ne_inr line 94