α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ n ∣ Multiset.lcm (cycleType σ)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ n ∣ orderOf σ
rw [← lcm_cycleType]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ cycleType σ
⊢ n ∣ Multiset.lcm (cycleType σ)
exact dvd_lcm h