mathlib3

5d4d8158 - feat(analysis): prove that a polynomial function is equivalent to its leading term along at_top, and consequences (#5354)

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. Co-authored-by: Patrick Massot <patrickmassot@free.fr>