no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ sum (cycleType σ) = Finset.card (support σ)
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => rw [hσ.cycleType, coe_sum, List.sum_singleton]
| induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]
no goals
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sum (cycleType 1) = Finset.card (support 1)
simp
no goals
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ sum (cycleType σ) = Finset.card (support σ)
rw [hσ.cycleType, coe_sum, List.sum_singleton]
no goals
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : sum (cycleType σ) = Finset.card (support σ)
hτ : sum (cycleType τ) = Finset.card (support τ)
⊢ sum (cycleType (σ * τ)) = Finset.card (support (σ * τ))
rw [hd.cycleType, sum_add, hσ, hτ, hd.card_support_mul]