Commit 2023-03-29 12:50 ad140a79

View on Github →

feat: port Topology.Algebra.Polynomial (#3168)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Polynomial.lean

added theorem Polynomial.coeff_bdd_of_roots_le

added theorem Polynomial.coeff_le_of_roots_le

added theorem Polynomial.eq_one_of_roots_le

added theorem Polynomial.exists_forall_norm_le

added theorem Polynomial.tendsto_abv_aeval_atTop

added theorem Polynomial.tendsto_abv_atTop

added theorem Polynomial.tendsto_abv_eval₂_atTop

added theorem Polynomial.tendsto_norm_atTop