English
Let f and g be commuting permutations of a set, and suppose g fixes a point x. Then the cycle of x under the product f∘g is the same as the cycle of x under f.
Русский
Пусть f и g — перестановки на множестве, которые коммутируют, и пусть g фиксирует точку x. Тогда цикл x для произведения f∘g совпадает с циклом x для f.
LaTeX
$$$\\\\forall \\\\alpha \\\\forall f,g \\\\in \\\\mathrm{Perm}(\\\\alpha), \\\\forall x \\\\in \\\\alpha, \\\\mathrm{Commute}(f,g) \land g(x)=x \\\\Rightarrow (f g).cycleOf x = f.cycleOf x$$$
Lean4
theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel f.SameCycle] [DecidableRel (f * g).SameCycle] (h : Commute f g)
(x : α) (hx : g x = x) : (f * g).cycleOf x = f.cycleOf x :=
by
ext y
by_cases hxy : (f * g).SameCycle x y
· obtain ⟨z, rfl⟩ := hxy
rw [cycleOf_apply_apply_zpow_self]
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
· rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
contrapose! hxy
obtain ⟨z, rfl⟩ := hxy
refine ⟨z, ?_⟩
simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]
