# Documentation

Mathlib.Data.Polynomial.DenomsClearable

# Denominators of evaluation of polynomials at ratios #

Let i : R → K be a homomorphism of semirings. Assume that K is commutative. If a and b are elements of R such that i b ∈ K is invertible, then for any polynomial f ∈ R[X] the "mathematical" expression b ^ f.natDegree * f (a / b) ∈ K is in the image of the homomorphism i.

def DenomsClearable {R : Type u_1} {K : Type u_2} [] [] (a : R) (b : R) (N : ) (f : ) (i : R →+* K) :

denomsClearable formalizes the property that b ^ N * f (a / b) does not have denominators, if the inequality f.natDegree ≤ N holds.

The definition asserts the existence of an element D of R and an element bi = 1 / i b of K such that clearing the denominators of the fraction equals i D.

Instances For
theorem denomsClearable_zero {R : Type u_1} {K : Type u_2} [] [] {i : R →+* K} {b : R} {bi : K} (N : ) (a : R) (bu : bi * i b = 1) :
DenomsClearable a b N 0 i
theorem denomsClearable_C_mul_X_pow {R : Type u_1} {K : Type u_2} [] [] {i : R →+* K} {b : R} {bi : K} {N : } (a : R) (bu : bi * i b = 1) {n : } (r : R) (nN : n N) :
DenomsClearable a b N (Polynomial.C r * Polynomial.X ^ n) i
theorem DenomsClearable.add {R : Type u_1} {K : Type u_2} [] [] {i : R →+* K} {a : R} {b : R} {N : } {f : } {g : } :
DenomsClearable a b N f iDenomsClearable a b N g iDenomsClearable a b N (f + g) i
theorem denomsClearable_of_natDegree_le {R : Type u_1} {K : Type u_2} [] [] {i : R →+* K} {b : R} {bi : K} (N : ) (a : R) (bu : bi * i b = 1) (f : ) :
DenomsClearable a b N f i
theorem denomsClearable_natDegree {R : Type u_1} {K : Type u_2} [] [] {b : R} {bi : K} (i : R →+* K) (f : ) (a : R) (bu : bi * i b = 1) :

If i : R → K is a ring homomorphism, f is a polynomial with coefficients in R, a, b are elements of R, with i b invertible, then there is a D ∈ R such that b ^ f.natDegree * f (a / b) equals i D.

theorem one_le_pow_mul_abs_eval_div {K : Type u_1} {f : } {a : } {b : } (b0 : 0 < b) (fab : Polynomial.eval (a / b) () 0) :
1 * |Polynomial.eval (a / b) ()|

Evaluating a polynomial with integer coefficients at a rational number and clearing denominators, yields a number greater than or equal to one. The target can be any LinearOrderedField K. The assumption on K could be weakened to LinearOrderedCommRing assuming that the image of the denominator is invertible in K.