# Zulip Chat Archive

## Stream: new members

### Topic: Computing with polynomials

#### Amos Turchet (Aug 11 2020 at 10:23):

I'm trying to prove the following lemma about lower bound for the value of a polynomial with integral coefficients evaluated at a rational number at a rational which is not a root of the polynomial. And I'm getting stuck and a bit worried:

```
import data.polynomial
import data.rat
notation α`[X]` := polynomial α
/-
The Lemma gives a lower bound on the absolute value of a polynomial f with integral coefficients evaluated at a rational number q which is not a root of f
-/
lemma poly_not_zero_low_bound (x : ℚ) (p : ℤ [X]) (hx : x.denom > 0) (hpx : polynomial.aeval x p ≠ 0) : abs(polynomial.aeval x p) ≥ 1 / (x.denom)^(p.nat_degree) :
begin
calc abs(polynomial.aeval x p) = abs((polynomial.aeval x p).num / (polynomial.aeval x p).denom) : by rw rat.num_denom (polynomial.aeval x p)
... = abs(polynomial.aeval x p).num / abs(polynomial.aeval x p).denom : by rw abs_div
... ≥ 1 / (abs(polynomial.aeval x p)).denom : by sorry --rw [hx, rat.mk_eq_zero, int.nat_abs_ne_zero_of_ne_zero]
... ≥ 1 / (x.denom)^(p.nat_degree) : by sorry
end
```

This was proven (a bit more generally) by @Jujian Zhang and it takes more than 100 lines of codes. To me it seems that the only *actual* computation to be done should be the last step which ideally would take less than that.

But before that it looks like I have issues with using `rat.num_denom`

as well as showing that given `hpx`

the numerator is a non-zero integer and therefore its absolute value is at least 1 (what David Masser calls the "Fundamental Theorem of Trascendence").

Last updated: May 13 2021 at 21:12 UTC