R : Type ?u.1604
inst✝ : Semiring R
f : R[X]
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
R : Type ?u.1604
inst✝ : Semiring R
f : R[X]
N : ℕ
⊢ Function.Injective (revAtFun N)
intro a b hab
no goals
R : Type ?u.1604
inst✝ : Semiring R
f : R[X]
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
rw [← @revAtFun_invol N a, hab, revAtFun_invol]