OAI/GroupTheory/Kervaire/PermutationCycles.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KervaireRibbon.Cycles line 14
2. def OAI.KervaireRibbon.numCycles line 15
3. def OAI.KervaireRibbon.cycleList line 16
4. lemma OAI.KervaireRibbon.cycleList_ne_nil line 19
5. lemma OAI.KervaireRibbon.cycleList_nodup line 23
6. lemma OAI.KervaireRibbon.mem_cycleList line 27
7. lemma OAI.KervaireRibbon.cycleList_next line 32
8. lemma OAI.KervaireRibbon.class_mem_cycleList line 41
9. def OAI.KervaireRibbon.cycleEquiv line 47
10. lemma OAI.KervaireRibbon.cycleEquiv_rotate line 66
11. lemma OAI.KervaireRibbon.exists_cycle_coordinates line 80

    Source documentation

    Every finite permutation has a literal decomposition into nonempty cyclic lists, including its fixed points.

    lemma exists_cycle_coordinates (σ : Equiv.Perm D) :
        ∃ (n : Cycles σ → ℕ) (e : (Σ z, Fin (n z+1)) ≃ D),
          ∀ z i, σ (e ⟨z,i⟩) = e ⟨z,finRotate (n z+1) i⟩ := by
    …

    Mentions: OAI.KervaireRibbon.Cycles

12. lemma OAI.KervaireRibbon.sameCycle_map_eq line 99
13. lemma OAI.KervaireRibbon.formPerm_cut line 109
14. lemma OAI.KervaireRibbon.mem_formPerm_of_fixed line 124
15. lemma OAI.KervaireRibbon.sameCycle_swap_separates line 134
16. lemma OAI.KervaireRibbon.sameCycle_swap_merges line 199
17. lemma OAI.KervaireRibbon.map_swap_eq line 227
18. lemma OAI.KervaireRibbon.sameCycle_transfer line 235
19. lemma OAI.KervaireRibbon.numCycles_eq_card line 248
20. lemma OAI.KervaireRibbon.numCycles_swap_merge line 263
21. lemma OAI.KervaireRibbon.numCycles_swap_split line 314