mathlib documentation

data.polynomial.denoms_clearable

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.nat_degree * f (a / b) ∈ K is in the image of the homomorphism i.

def denoms_clearable {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] (a b : R) (N : ) (f : polynomial R) (i : R →+* K) :
Prop

denoms_clearable formalizes the property that b ^ N * f (a / b) does not have denominators, if the inequality f.nat_degree ≤ 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
theorem denoms_clearable_zero {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] {i : R →+* K} {b : R} {bi : K} (N : ) (a : R) (bu : bi * i b = 1) :
theorem denoms_clearable_C_mul_X_pow {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] {i : R →+* K} {b : R} {bi : K} {N : } (a : R) (bu : bi * i b = 1) {n : } (r : R) (nN : n N) :
theorem denoms_clearable.add {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] {i : R →+* K} {a b : R} {N : } {f g : polynomial R} :
denoms_clearable a b N f idenoms_clearable a b N g idenoms_clearable a b N (f + g) i
theorem denoms_clearable_of_nat_degree_le {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] {i : R →+* K} {b : R} {bi : K} (N : ) (a : R) (bu : bi * i b = 1) (f : polynomial R) :
f.nat_degree Ndenoms_clearable a b N f i
theorem denoms_clearable_nat_degree {R : Type u_1} {K : Type u_2} [semiring R] [comm_semiring K] {b : R} {bi : K} (i : R →+* K) (f : polynomial R) (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.nat_degree * f (a / b) equals i D.

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 linear_ordered_field K. The assumption on K could be weakened to linear_ordered_comm_ring assuming that the image of the denominator is invertible in K.