cycleOf_ne_one_iff_mem_cycleFactorsFinset

English

cycleOf g x is nontrivial if and only if it belongs to the cycle factors of g.

Русский

cycleOf g x не тривиален тогда и только тогда, когда принадлежит фактору циклa g.

LaTeX

$$$cycleOf(g,x) \neq 1 \iff cycleOf(g,x) \in cycleFactorsFinset(g)$$$

Lean4

theorem cycleOf_ne_one_iff_mem_cycleFactorsFinset {g : Equiv.Perm α} {x : α} :
    g.cycleOf x ≠ 1 ↔ g.cycleOf x ∈ g.cycleFactorsFinset := by
  rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, ne_eq, cycleOf_eq_one_iff]

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