α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ (-1) ^ (sum {3} + ↑card {3}) = 1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ ↑Perm.sign σ = 1
rw [Equiv.Perm.sign_of_cycleType, h.cycleType]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : IsThreeCycle σ
⊢ (-1) ^ (sum {3} + ↑card {3}) = 1
rfl