no goals
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = 1
⊢ ↑sign 1 = a
simp [h]
no goals
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ ↑sign (swap x y) = a
rw [sign_swap hxy, h]