Commit 2021-02-07 21:13 5d4d8158

feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354) The main result is eval_is_equivalent_at_top_eval_lead, which states that for any polynomial P of degree n with leading coeff a, the corresponding polynomial function is equivalent to a * x^n as x goes to +∞. We can then use this result to prove various limits for polynomial and rational functions, depending on the degrees and leading coeffs of the considered polynomials.