Documentation

Mathlib.Algebra.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} [Semiring R] [CommSemiring K] (a : R) (b : R) (N : ) (f : Polynomial R) (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.

Equations
Instances For
    theorem denomsClearable_zero {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {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} [Semiring R] [CommSemiring K] {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} [Semiring R] [CommSemiring K] {i : R →+* K} {a : R} {b : R} {N : } {f : Polynomial R} {g : Polynomial R} :
    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} [Semiring R] [CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ) (a : R) (bu : bi * i b = 1) (f : Polynomial R) :
    f.natDegree NDenomsClearable a b N f i
    theorem denomsClearable_natDegree {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {b : R} {bi : K} (i : R →+* K) (f : Polynomial R) (a : R) (bu : bi * i b = 1) :
    DenomsClearable a b f.natDegree f i

    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} [LinearOrderedField K] {f : Polynomial } {a : } {b : } (b0 : 0 < b) (fab : Polynomial.eval (a / b) (Polynomial.map (algebraMap K) f) 0) :
    1 b ^ f.natDegree * |Polynomial.eval (a / b) (Polynomial.map (algebraMap K) f)|

    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.