mathlib3 documentation

data.polynomial.denoms_clearable

Denominators of evaluation of polynomials at ratios #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
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
source
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) :
denoms_clearable a b N 0 i
source
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) :
denoms_clearable a b N (⇑polynomial.C r * polynomial.X ^ n) i
source
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 i → denoms_clearable a b N g i → denoms_clearable a b N (f + g) i
source
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 ≤ N → denoms_clearable a b N f i
source
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) :
denoms_clearable a b f.nat_degree 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.nat_degree * f (a / b) equals i D.

source
theorem one_le_pow_mul_abs_eval_div {K : Type u_1} [linear_ordered_field K] {f : polynomial ℤ} {a b : ℤ} (b0 : 0 < b) (fab : polynomial.eval (↑a / ↑b) (polynomial.map (algebra_map ℤ K) f) ≠ 0) :
1 ≤ ↑b ^ f.nat_degree * |polynomial.eval (↑a / ↑b) (polynomial.map (algebra_map ℤ 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 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.