English
If f and g are disjoint permutations, then the cycle of x under the product f∘g equals the product of the cycles of x under f and under g.
Русский
Если f и g — попарно непересекающиеся перестановки, то цикл x для произведения f∘g равен произведению циклов x для f и для g.
LaTeX
$$$\\\\forall \\alpha \\, f,g \\\\in \\\\mathrm{Perm}(\\\\alpha), \\\\forall x \\\\in \\\\alpha, \\\\mathrm{Disjoint}(f,g) \\\\Rightarrow (f g).cycleOf x = f.cycleOf x \\\\cdot g.cycleOf x$$$
Lean4
theorem cycleOf_mul_distrib [DecidableRel f.SameCycle] [DecidableRel g.SameCycle] [DecidableRel (f * g).SameCycle]
[DecidableRel (g * f).SameCycle] (h : f.Disjoint g) (x : α) : (f * g).cycleOf x = f.cycleOf x * g.cycleOf x :=
by
rcases (disjoint_iff_eq_or_eq.mp h) x with hfx | hgx
· simp [h.commute.eq, cycleOf_mul_of_apply_right_eq_self h.symm.commute, hfx]
· simp [cycleOf_mul_of_apply_right_eq_self h.commute, hgx]
