no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
| induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]
no goals
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ↑sign 1 = prod (map (fun n => -(-1) ^ n) (cycleType 1))
simp
no goals
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : IsCycle σ
⊢ ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
simp [hσ.cycleType, hσ.sign]
no goals
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : Disjoint σ τ
a✝ : IsCycle σ
hσ : ↑sign σ = prod (map (fun n => -(-1) ^ n) (cycleType σ))
hτ : ↑sign τ = prod (map (fun n => -(-1) ^ n) (cycleType τ))
⊢ ↑sign (σ * τ) = prod (map (fun n => -(-1) ^ n) (cycleType (σ * τ)))
simp [hσ, hτ, hd.cycleType]