cycleFactorsFinset_eq_finset — Mathlib

English

Equivalence between a finset factorization and a list factorization of a permutation’s cycle decomposition.

Русский

Эквивалентность между разложением на циклы в виде списка и множества.

LaTeX

$$$cycleFactorsFinset (f) = s \\iff \\text{(conditions on s as a list of cycles and their prod equals f)}$$$

Lean4

theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
    σ.cycleFactorsFinset = s ↔
      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
        ∃ h : (s : Set (Perm α)).Pairwise Disjoint, s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ :=
  by
  obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq
  simp [cycleFactorsFinset_eq_list_toFinset, hl]

Похожие утверждения