Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 10:30 c488997d

View on Github →

feat(analysis/special_functions/polynomial): polynomials are big O of polynomials of higher degree (#6714)

Estimated changes

Modified src/analysis/asymptotics/asymptotics.lean

added theorem asymptotics.div_is_bounded_under_of_is_O

added theorem asymptotics.is_O_iff_div_is_bounded_under

added theorem asymptotics.is_O_of_div_tendsto_nhds

Modified src/analysis/normed_space/basic.lean

added theorem is_bounded_under_of_tendsto

added theorem norm_le_norm_add_const_of_dist_le

added theorem norm_lt_norm_add_const_of_dist_lt

Modified src/analysis/special_functions/polynomials.lean

added theorem polynomial.eventually_no_roots

added theorem polynomial.is_O_of_degree_le

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.ne_zero_of_degree_ge_degree

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.exists_max_root

added theorem polynomial.exists_min_root

Modified src/data/set/finite.lean

added theorem set.exists_lower_bound_image

added theorem set.exists_upper_bound_image