Commit 2021-02-10 21:01 56fde49b

feat(data/polynomial/denoms_clearable): add lemma about clearing denominators in evaluating a polynomial (#6122) 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. Reference: Liouville PR #4301.