Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 21:29 866664b8

View on Github →

feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670) Add three lemmas about polynomials needed for #15143 From flt-regular

Estimated changes

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

added theorem polynomial.ext_iff_degree_le

added theorem polynomial.ext_iff_nat_degree_le

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.bUnion_roots_finite

Modified src/topology/algebra/polynomial.lean

added theorem polynomial.coeff_bdd_of_roots_le

added theorem polynomial.eq_one_of_roots_le