α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ -1 ≠ 1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ List.prod l ∈ alternatingGroup α ↔ Even (List.length l)
rw [mem_alternatingGroup, sign_prod_list_swap hl, ← Units.val_eq_one, Units.val_pow_eq_pow_val,
  Units.coe_neg_one, neg_one_pow_eq_one_iff_even]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ -1 ≠ 1
decide