orderOf_cycleOf_dvd_orderOf — Mathlib

English

The order of the cycle containing x divides the order of the permutation: orderOf (cycleOf f x) ∣ orderOf f.

Русский

Порядок цикла, содержащего x, делит порядок перестановки: orderOf(cycleOf f x) ∣ orderOf f.

LaTeX

$$$$\operatorname{orderOf}(\mathrm{cycleOf}(f, x)) \mid \operatorname{orderOf}(f).$$$$

Lean4

theorem orderOf_cycleOf_dvd_orderOf (f : Perm α) (x : α) : orderOf (cycleOf f x) ∣ orderOf f :=
  by
  by_cases hx : f x = x
  · rw [← cycleOf_eq_one_iff] at hx
    simp [hx]
  · refine dvd_of_mem_cycleType ?_
    rw [cycleType, Multiset.mem_map]
    refine ⟨f.cycleOf x, ?_, ?_⟩
    · rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
    · simp [(isCycle_cycleOf _ hx).orderOf]

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