OAI/GroupTheory/Kervaire/Circles.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireRibbon.Circle line 14
2. lemma OAI.KervaireRibbon.chain_mem_next line 18
3. lemma OAI.KervaireRibbon.circle_cycles line 33
4. lemma OAI.KervaireRibbon.circle_mem_apply line 56
5. lemma OAI.KervaireRibbon.sameCycle_two line 61
6. lemma OAI.KervaireRibbon.chain_cap line 71
7. abbrev OAI.KervaireRibbon.FreeProd line 104
8. def OAI.KervaireRibbon.dartLetter line 105
9. def OAI.KervaireRibbon.dartEval line 107
10. lemma OAI.KervaireRibbon.dartEval_append line 109
11. lemma OAI.KervaireRibbon.dartEval_cons line 112
12. lemma OAI.KervaireRibbon.dart_pinch line 117

    Source documentation

    An actual adjacent cancellable unit pair in a coefficient-valued outside word. Nothing about coefficients being finite or torsion-free is used.

    lemma dart_pinch (t : D → ℤ) (c : D → A) (l : List D) (hl : l ≠ [])
        (ht : ∀ d ∈ l, t d = 1 ∨ t d = -1) (g : A)
        (he : dartEval t c l = Coprod.inl g) :
        ∃ pre post x y, l = pre ++ x::y::post ∧ c x = 1 ∧ t y = -t x := by
    …

    Mentions: OAI.KervaireRibbon.dartEval