no goals
α : Type u_1
β : Type u_2
γ : Type ?u.25765
δ : Type ?u.25768
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type ?u.25777
G : Type ?u.25780
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
e : α ≃* β
h : Prime p
a : β
⊢ ↑e (↑(symm e) a) = a
simp
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.25765
δ : Type ?u.25768
inst✝³ : CommMonoidWithZero α
inst✝² : CommMonoidWithZero β
F : Type ?u.25777
G : Type ?u.25780
inst✝¹ : MonoidWithZeroHomClass F α β
inst✝ : MulHomClass G β α
f : F
g : G
p : α
e : α ≃* β
a : α
⊢ ↑(symm e) (↑e a) = a
simp