Commit 2021-01-27 08:41 00b88eb1

feat(data/polynomial/denominators): add file denominators (#5587) The main goal of this PR is to establish that b^deg(f)*f(a/b) is an expression not involving denominators. The first lemma, induction_with_nat_degree_le is an induction principle for polynomials, where the inductive hypothesis has a bound on the degree of the polynomial. This allows to build the proof by tearing apart a polynomial into its monomials, while remembering the overall degree of the polynomial itself. This lemma might be a better fit for the file data.polynomial.induction.