OAI/RingTheory/DirectFiniteness/VertexMerging.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.mergeWhite_components line 16
  2. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_mergeWhite line 31
  3. def OAI.KaplanskyCounterexample.Planar.Ribbon.mergeBlack line 46

    Source documentation

    The color-reversed local surgery.

    def Ribbon.mergeBlack (R : Ribbon α) (a : α) : Ribbon α where
…

    Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

  4. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.mergeBlack_face line 51
  5. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.mergeBlack_components line 57
  6. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_mergeBlack line 73
  7. lemma OAI.KaplanskyCounterexample.Planar.label_swap line 89
  8. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.mergeWhite line 101
  9. def OAI.KaplanskyCounterexample.Planar.WeakBalanced.mergeBlack line 114