mathlib

00b88eb1 - feat(data/polynomial/denominators): add file denominators (#5587)

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`.