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) = 0 iff eval₂ i x f = 0.
Русский
Пусть i: R →+* S — гомоморфизм колец, и x ∈ S обратим. Для N и f ∈ R[X] с natDegree f ≤ N выполняется: eval₂ i (⅟x) (reflect N f) = 0 ⇔ eval₂ i x f = 0.
LaTeX
$$$\operatorname{eval}_i\left(\tfrac{1}{x}\right)\big(\operatorname{reflect}_N f\big) = 0 \;\iff\; \operatorname{eval}_i(x) f = 0.$$$
Lean4
theorem eval₂_reflect_eq_zero_iff (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X]) (hf : f.natDegree ≤ N) :
eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0 :=
by
conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
constructor
· intro h
rw [h, zero_mul]
· intro h
rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h, zero_mul]
