no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.lcm (cycleType σ) = orderOf σ
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, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]
no goals
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ Multiset.lcm (cycleType 1) = orderOf 1
simp
no goals
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ Multiset.lcm (cycleType σ) = orderOf σ
simp [hσ.cycleType, hσ.orderOf]
no goals
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : Multiset.lcm (cycleType σ) = orderOf σ
hτ : Multiset.lcm (cycleType τ) = orderOf τ
⊢ Multiset.lcm (cycleType (σ * τ)) = orderOf (σ * τ)
simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]