OAI/RingTheory/DirectFiniteness/BoundaryCycles.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KaplanskyCounterexample.Planar.Follows line 16

    Source documentation

    The listed distinct edges constitute a whole rotation cycle.

    def Follows (p : Perm α) (l : List α) : Prop := ∀ x ∈ l, p x = l.formPerm x
…
  2. lemma OAI.KaplanskyCounterexample.Planar.Follows.invariant line 19
  3. lemma OAI.KaplanskyCounterexample.Planar.Follows.sameCycle line 34
  4. lemma OAI.KaplanskyCounterexample.Planar.Follows.cycleSet line 45
  5. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_iff_of_eqOn_cycle line 56
  6. lemma OAI.KaplanskyCounterexample.Planar.cycleSet_eq_of_eqOn_cycle line 75
  7. lemma OAI.KaplanskyCounterexample.Planar.formPerm_map_apply line 83
  8. lemma OAI.KaplanskyCounterexample.Planar.Follows.map_sum_left line 98