α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) (cycleType f)) = (-1) ^ (sum (cycleType f) + ↑card (cycleType f))
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ ↑sign f = (-1) ^ (sum (cycleType f) + ↑card (cycleType f))
rw [sign_of_cycleType']
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) 0) = (-1) ^ (sum 0 + ↑card 0)

case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ prod (map (fun n => -(-1) ^ n) (a ::ₘ s)) = (-1) ^ (sum (a ::ₘ s) + ↑card (a ::ₘ s))
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) (cycleType f)) = (-1) ^ (sum (cycleType f) + ↑card (cycleType f))
induction' f.cycleType using Multiset.induction_on with a s ihs
no goals
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ prod (map (fun n => -(-1) ^ n) 0) = (-1) ^ (sum 0 + ↑card 0)
rfl
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ -(-1) ^ a * (-1) ^ (sum s + ↑card s) = (-1) ^ (a + sum s + (↑card s + 1))
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ prod (map (fun n => -(-1) ^ n) (a ::ₘ s)) = (-1) ^ (sum (a ::ₘ s) + ↑card (a ::ₘ s))
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.sum_cons, Multiset.card_cons, ihs]
no goals
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : prod (map (fun n => -(-1) ^ n) s) = (-1) ^ (sum s + ↑card s)
⊢ -(-1) ^ a * (-1) ^ (sum s + ↑card s) = (-1) ^ (a + sum s + (↑card s + 1))
simp only [pow_add, pow_one, mul_neg_one, neg_mul, mul_neg, mul_assoc, mul_one]