English
Let i: R →+* S be a ring homomorphism and x ∈ S invertible. For N ∈ ℕ and f ∈ R[X] with natDegree f ≤ N, we have eval₂ i (⅟x) (reflect N f) · x^N = eval₂ i x f.
Русский
Пусть i: R →+* S — гомоморфизм колец, и x ∈ S является обратимым. Для N ∈ ℕ и f ∈ R[X] с natDegree f ≤ N выполняется равенство: eval₂ i (⅟x) (reflect N f) · x^N = eval₂ i x f.
LaTeX
$$$\operatorname{eval}_i\left(\tfrac{1}{x}\right)\big(\operatorname{reflect}_N f\big) \cdot x^{N} = \operatorname{eval}_i(x) f.$$$
Lean4
theorem eval₂_reflect_mul_pow (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X]) (hf : f.natDegree ≤ N) :
eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f :=
by
refine induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_ ?_ f hf
· simp
· intro n r _ hnN
simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
· intros
simp [*, add_mul]
