OAI/RingTheory/DirectFiniteness/RibbonSums.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.Planar.sumSetoid line 15
  2. lemma OAI.KaplanskyCounterexample.Planar.sumSetoid_inl line 18
  3. lemma OAI.KaplanskyCounterexample.Planar.sumSetoid_inr line 23
  4. lemma OAI.KaplanskyCounterexample.Planar.sumSetoid_cross line 28
  5. def OAI.KaplanskyCounterexample.Planar.sumSetoidEquiv line 33
  6. lemma OAI.KaplanskyCounterexample.Planar.sumSetoid_card line 42
  7. lemma OAI.KaplanskyCounterexample.Planar.sumSetoid_le line 46
  8. lemma OAI.KaplanskyCounterexample.Planar.sumCongr_cycles_setoid line 57
  9. lemma OAI.KaplanskyCounterexample.Planar.sumCongr_cycles_card line 74
  10. def OAI.KaplanskyCounterexample.Planar.Ribbon.sum line 79
  11. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.sum_face line 83
  12. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.sum_components line 88
  13. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_sum line 108
  14. lemma OAI.KaplanskyCounterexample.Planar.formPerm_append_nonempty line 118