α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ signAux 1 = 1
unfold signAux
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = ∏ _x in finPairsLT n, 1
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
conv => rhs; rw [← @Finset.prod_const_one ℤˣ _ (finPairsLT n)]
no goals
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = ∏ _x in finPairsLT n, 1
exact Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_le