lcm_cycleType — Mathlib

English

The least common multiple of the cycle lengths equals the order of the permutation: lcm(σ.cycleType) = orderOf σ.

Русский

Наименьшее общее кратное длин циклов равно порядка перестановки: lcm(σ.cycleType) = orderOf σ.

LaTeX

$$$$\mathrm{lcm}(\sigma.\mathrm{cycleType}) = \mathrm{orderOf}(\sigma).$$$$

Lean4

@[simp]
theorem lcm_cycleType (σ : Perm α) : σ.cycleType.lcm = orderOf σ := by
  induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
  | induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType_mul, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

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