OAI/RingTheory/DirectFiniteness/CycleFactorization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.Planar.sameCycle_map_quotient line 16
2. lemma OAI.KaplanskyCounterexample.Planar.swap_cycles_card_le line 22
3. lemma OAI.KaplanskyCounterexample.Planar.cycles_card_le line 48
4. lemma OAI.KaplanskyCounterexample.Planar.cycles_one_card line 51
5. lemma OAI.KaplanskyCounterexample.Planar.exists_cycle_factorization line 60

   Source documentation

   A minimal transposition factorization, with each transposition contained in one of the original cycles.

   lemma exists_cycle_factorization (p : Perm α) :
       ∃ l : List (α × α),
         (l.map fun ab => swap ab.1 ab.2).prod = p ∧
         l.length + Nat.card (Cycles p) = Fintype.card α ∧
         ∀ ab ∈ l, ab.1 ≠ ab.2 ∧ p.SameCycle ab.1 ab.2 := by
   …

   Mentions: OAI.KaplanskyCounterexample.Planar.Cycles