Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-29 12:26 e003d6e2

View on Github →

feat(data/polynomial): more API for roots (#11081) leading_coeff_monic_mul leading_coeff_X_sub_C root_multiplicity_C not_is_root_C roots_smul_nonzero leading_coeff_div_by_monic_X_sub_C roots_eq_zero_iff also generalized various statements about X - C a to X + C a over semirings.

Estimated changes

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

added theorem polynomial.X_add_C_ne_zero

added theorem polynomial.X_pow_add_C_ne_zero

modified theorem polynomial.degree_X_add_C

added theorem polynomial.degree_X_pow_add_C

added theorem polynomial.leading_coeff_C_mul_X_add_C

modified theorem polynomial.leading_coeff_X_add_C

added theorem polynomial.leading_coeff_X_pow_add_C

added theorem polynomial.leading_coeff_X_pow_add_one

added theorem polynomial.leading_coeff_X_sub_C

added theorem polynomial.nat_degree_X_add_C

added theorem polynomial.nat_degree_X_pow_add_C

added theorem polynomial.next_coeff_X_add_C

modified theorem polynomial.next_coeff_X_sub_C

added theorem polynomial.zero_nmem_multiset_map_X_add_C

Modified src/data/polynomial/div.lean

added theorem polynomial.root_multiplicity_C

Modified src/data/polynomial/eval.lean

added theorem polynomial.not_is_root_C

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.leading_coeff_div_by_monic_X_sub_C

added theorem polynomial.roots_smul_nonzero

Modified src/field_theory/is_alg_closed/basic.lean

added theorem is_alg_closed.roots_eq_zero_iff