OAI/RingTheory/DirectFiniteness/RibbonWheels.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Planar.Ribbon.wheel line 17

   Source documentation

   A planar two-vertex wheel: opposite rotations and matching white bivalent vertices. Empty and singleton rotations are included.

   def Ribbon.wheel (p : Perm α) : Ribbon (α ⊕ α) :=
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Ribbon

2. def OAI.KaplanskyCounterexample.Planar.sumIndex line 20
3. def OAI.KaplanskyCounterexample.Planar.wheelFaceIndex line 22
4. lemma OAI.KaplanskyCounterexample.Planar.wheel_white_index line 25
5. lemma OAI.KaplanskyCounterexample.Planar.wheel_face_index line 29
6. lemma OAI.KaplanskyCounterexample.Planar.wheel_white_setoid line 33
7. lemma OAI.KaplanskyCounterexample.Planar.wheel_face_setoid line 45
8. lemma OAI.KaplanskyCounterexample.Planar.wheel_component_index line 69
9. lemma OAI.KaplanskyCounterexample.Planar.wheel_white_card line 97
10. lemma OAI.KaplanskyCounterexample.Planar.wheel_face_card line 103
11. lemma OAI.KaplanskyCounterexample.Planar.wheel_component_card line 109
12. lemma OAI.KaplanskyCounterexample.Planar.Ribbon.genusZero_wheel line 118