α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
hg : g = (e.symm.trans f).trans e
⊢ ↑sign f = ↑sign g
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
⊢ ↑sign f = ↑sign g
have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
hg : g = (e.symm.trans f).trans e
⊢ ↑sign f = ↑sign g
rw [hg, sign_symm_trans_trans]
no goals
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
⊢ ∀ (x : β), ↑g x = ↑((e.symm.trans f).trans e) x
simp [h]