cycleFactorsFinset_mem_commute' — Mathlib

English

If g1 and g2 are cycle factors of f, then g1 and g2 commute.

Русский

Если g1 и g2 — цикловые факторы f, то они коммутируют.

LaTeX

$$∀ {g1 g2} (h1 : g1 ∈ cycleFactorsFinset) (h2 : g2 ∈ cycleFactorsFinset), Commute g1 g2$$

Lean4

/-- Two cycles of a permutation commute. -/
theorem cycleFactorsFinset_mem_commute' {g1 g2 : Perm α} (h1 : g1 ∈ f.cycleFactorsFinset)
    (h2 : g2 ∈ f.cycleFactorsFinset) : Commute g1 g2 :=
  by
  rcases eq_or_ne g1 g2 with rfl | h
  · apply Commute.refl
  · exact Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h

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