one_le_pow_mul_abs_eval_div
theorem one_le_pow_mul_abs_eval_div :
∀ {K : Type u_1} [inst : LinearOrderedField K] {f : Polynomial ℤ} {a b : ℤ},
0 < b →
Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0 →
1 ≤ ↑b ^ f.natDegree * |Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|
This theorem states that when evaluating a polynomial with integer coefficients at a rational number and subsequently clearing the denominators, the resulting value is a number that is greater than or equal to one. This condition holds for any target of type `K` that is a LinearOrderedField. The assumption on `K` can be weakened to a `LinearOrderedCommRing` assuming that the image of the denominator is invertible in `K`. Specifically, given a polynomial `f`, and integers `a` and `b` such that `b` is positive, if the evaluation of the polynomial (after mapping through the algebraMap from integers to `K`) at `a/b` is non-zero, then the absolute value of this evaluation, multiplied by `b` raised to the power of the degree of the polynomial, is at least one.
More concisely: For any LinearOrderedField `K` and polynomial `f` with integer coefficients, the absolute value of evaluating `f` at a rational number `a/b` and clearing denominators results in a value greater than or equal to `b^(deg(f))` if `b` is positive and the evaluation is non-zero.
|
denomsClearable_natDegree
theorem denomsClearable_natDegree :
∀ {R : Type u_1} {K : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring K] {b : R} {bi : K} (i : R →+* K)
(f : Polynomial R) (a : R), bi * i b = 1 → DenomsClearable a b f.natDegree f i
This theorem states that if `i` is a function that is a ring homomorphism from `R` to `K`, `f` is a polynomial with coefficients in `R`, and `a, b` are elements of `R` where the image of `b` under `i` is invertible (i.e., `bi * i b = 1`), then there exists an element `D` in `R` such that the expression `b` to the power of the degree of `f` times the evaluation of `f` at `a / b` equals the image of `D` under `i`. This theorem is related to the process of making the denominators of a rational function clearable, in the context of algebraic number fields.
More concisely: If `i` is a ring homomorphism from `R` to `K`, `f` is a polynomial with coefficients in `R`, `a, b` are in `R` with `b i b = 1`, then there exists `D` in `R` such that `(b^(deg f)) * (f a / b) = i D`.
|