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
.
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
- denoms_clearable a b N f i = ∃ (D : R) (bi : K), bi * ⇑i b = 1 ∧ ⇑i D = ⇑i b ^ N * polynomial.eval (⇑i a * bi) (polynomial.map i f)
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
.