no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : x = y
⊢ ↑sign (swap x y) = if x = y then 1 else -1
simp [H, swap_self]
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : ¬x = y
⊢ ↑sign (swap x y) = if x = y then 1 else -1
simp [sign_swap H, H]