Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-16 19:13 33d45bf0

View on Github →

chore(data/polynomial): break up behemoth file (#3407) Polynomial refactor The goal is to split data/polynomial.lean into several self-contained files in the same place. For the time being, the new place for all these files is data/polynomial/. Future PRs may simplify proofs, remove duplicate lemmas, and move files out of the data directory.

Estimated changes

Deleted src/data/polynomial.lean

deleted theorem is_integral_domain.polynomial

deleted def polynomial.C

deleted theorem polynomial.C_0

deleted theorem polynomial.C_1

deleted theorem polynomial.C_add

deleted theorem polynomial.C_bit0

deleted theorem polynomial.C_bit1

deleted theorem polynomial.C_comp

deleted theorem polynomial.C_eq_algebra_map

deleted theorem polynomial.C_eq_int_cast

deleted theorem polynomial.C_eq_nat_cast

deleted theorem polynomial.C_inj

deleted theorem polynomial.C_mul'

deleted theorem polynomial.C_mul

deleted theorem polynomial.C_neg

deleted theorem polynomial.C_pow

deleted theorem polynomial.C_sub

deleted def polynomial.X

deleted theorem polynomial.X_comp

deleted theorem polynomial.X_dvd_iff

deleted theorem polynomial.X_mul

deleted theorem polynomial.X_ne_zero

deleted theorem polynomial.X_pow_mul

deleted theorem polynomial.X_pow_mul_assoc

deleted theorem polynomial.X_pow_sub_C_ne_zero

deleted theorem polynomial.X_sub_C_ne_zero

deleted theorem polynomial.add_comp

deleted def polynomial.aeval

deleted theorem polynomial.aeval_C

deleted theorem polynomial.aeval_X

deleted theorem polynomial.aeval_alg_hom

deleted theorem polynomial.aeval_alg_hom_apply

deleted theorem polynomial.aeval_def

deleted theorem polynomial.alg_hom_eval₂_algebra_map

deleted theorem polynomial.algebra_map_apply

deleted theorem polynomial.apply_eq_coeff

deleted theorem polynomial.as_sum

deleted def polynomial.binom_expansion

deleted theorem polynomial.card_nth_roots

deleted theorem polynomial.card_roots'

deleted theorem polynomial.card_roots

deleted theorem polynomial.card_roots_X_pow_sub_C

deleted theorem polynomial.card_roots_sub_C'

deleted theorem polynomial.card_roots_sub_C

deleted theorem polynomial.coe_eval₂_ring_hom

deleted theorem polynomial.coe_norm_unit

deleted def polynomial.coeff

deleted theorem polynomial.coeff_C

deleted theorem polynomial.coeff_C_mul

deleted theorem polynomial.coeff_C_mul_X

deleted theorem polynomial.coeff_C_zero

deleted theorem polynomial.coeff_X

deleted theorem polynomial.coeff_X_one

deleted theorem polynomial.coeff_X_pow

deleted theorem polynomial.coeff_X_zero

deleted theorem polynomial.coeff_add

deleted def polynomial.coeff_coe_to_fun

deleted theorem polynomial.coeff_coe_units_zero_ne_zero

deleted theorem polynomial.coeff_comp_degree_mul_degree

deleted theorem polynomial.coeff_derivative

deleted theorem polynomial.coeff_eq_zero_of_degree_lt

deleted theorem polynomial.coeff_eq_zero_of_nat_degree_lt

deleted theorem polynomial.coeff_inv_units

deleted theorem polynomial.coeff_map

deleted theorem polynomial.coeff_mk

deleted theorem polynomial.coeff_monomial_mul

deleted theorem polynomial.coeff_monomial_zero_mul

deleted theorem polynomial.coeff_mul

deleted theorem polynomial.coeff_mul_C

deleted theorem polynomial.coeff_mul_X

deleted theorem polynomial.coeff_mul_X_pow

deleted theorem polynomial.coeff_mul_X_sub_C

deleted theorem polynomial.coeff_mul_X_zero

deleted theorem polynomial.coeff_mul_degree_add_degree

deleted theorem polynomial.coeff_mul_monomial

deleted theorem polynomial.coeff_mul_monomial_zero

deleted theorem polynomial.coeff_nat_degree_eq_zero_of_degree_lt

deleted theorem polynomial.coeff_nat_degree_succ_eq_zero

deleted theorem polynomial.coeff_ne_zero_of_eq_degree

deleted theorem polynomial.coeff_neg

deleted theorem polynomial.coeff_one

deleted theorem polynomial.coeff_one_zero

deleted theorem polynomial.coeff_single

deleted theorem polynomial.coeff_smul

deleted theorem polynomial.coeff_sub

deleted theorem polynomial.coeff_sum

deleted theorem polynomial.coeff_zero

deleted theorem polynomial.coeff_zero_eq_eval_zero

deleted def polynomial.comp

deleted theorem polynomial.comp_C

deleted theorem polynomial.comp_X

deleted theorem polynomial.comp_one

deleted theorem polynomial.comp_zero

deleted def polynomial.decidable_dvd_monic

deleted def polynomial.degree

deleted theorem polynomial.degree_C

deleted theorem polynomial.degree_C_le

deleted theorem polynomial.degree_C_mul_X_pow_le

deleted theorem polynomial.degree_X

deleted theorem polynomial.degree_X_le

deleted theorem polynomial.degree_X_pow

deleted theorem polynomial.degree_X_pow_le

deleted theorem polynomial.degree_X_pow_sub_C

deleted theorem polynomial.degree_X_sub_C

deleted theorem polynomial.degree_add_C

deleted theorem polynomial.degree_add_div

deleted theorem polynomial.degree_add_div_by_monic

deleted theorem polynomial.degree_add_eq_of_degree_lt

deleted theorem polynomial.degree_add_eq_of_leading_coeff_add_ne_zero

deleted theorem polynomial.degree_add_le

deleted theorem polynomial.degree_coe_units

deleted theorem polynomial.degree_derivative_eq

deleted theorem polynomial.degree_derivative_le

deleted theorem polynomial.degree_derivative_lt

deleted theorem polynomial.degree_div_X_lt

deleted theorem polynomial.degree_div_by_monic_le

deleted theorem polynomial.degree_div_by_monic_lt

deleted theorem polynomial.degree_div_le

deleted theorem polynomial.degree_div_lt

deleted theorem polynomial.degree_eq_bot

deleted theorem polynomial.degree_eq_degree_of_associated

deleted theorem polynomial.degree_eq_iff_nat_degree_eq

deleted theorem polynomial.degree_eq_iff_nat_degree_eq_of_pos

deleted theorem polynomial.degree_eq_nat_degree

deleted theorem polynomial.degree_eq_one_of_irreducible_of_root

deleted theorem polynomial.degree_eq_zero_of_is_unit

deleted theorem polynomial.degree_erase_le

deleted theorem polynomial.degree_erase_lt

deleted theorem polynomial.degree_le_degree

deleted theorem polynomial.degree_le_iff_coeff_zero

deleted theorem polynomial.degree_le_mul_left

deleted theorem polynomial.degree_le_nat_degree

deleted theorem polynomial.degree_le_zero_iff

deleted theorem polynomial.degree_lt_degree_mul_X

deleted theorem polynomial.degree_lt_wf

deleted theorem polynomial.degree_map'

deleted theorem polynomial.degree_map

deleted theorem polynomial.degree_map_eq_of_injective

deleted theorem polynomial.degree_map_eq_of_leading_coeff_ne_zero

deleted theorem polynomial.degree_map_le

deleted theorem polynomial.degree_mod_by_monic_le

deleted theorem polynomial.degree_mod_by_monic_lt

deleted theorem polynomial.degree_monomial

deleted theorem polynomial.degree_monomial_le

deleted theorem polynomial.degree_mul_eq'

deleted theorem polynomial.degree_mul_eq

deleted theorem polynomial.degree_mul_le

deleted theorem polynomial.degree_mul_leading_coeff_inv

deleted theorem polynomial.degree_ne_of_nat_degree_ne

deleted theorem polynomial.degree_neg

deleted theorem polynomial.degree_nonneg_iff_ne_zero

deleted theorem polynomial.degree_normalize

deleted theorem polynomial.degree_one

deleted theorem polynomial.degree_one_le

deleted theorem polynomial.degree_pos_induction_on

deleted theorem polynomial.degree_pos_of_aeval_root

deleted theorem polynomial.degree_pos_of_eval₂_root

deleted theorem polynomial.degree_pos_of_ne_zero_of_nonunit

deleted theorem polynomial.degree_pos_of_root

deleted theorem polynomial.degree_pow_eq'

deleted theorem polynomial.degree_pow_eq

deleted theorem polynomial.degree_pow_le

deleted theorem polynomial.degree_sub_le

deleted theorem polynomial.degree_sub_lt

deleted theorem polynomial.degree_sum_le

deleted theorem polynomial.degree_zero

deleted def polynomial.derivative

deleted theorem polynomial.derivative_C

deleted theorem polynomial.derivative_X

deleted theorem polynomial.derivative_add

deleted theorem polynomial.derivative_eval

deleted theorem polynomial.derivative_eval₂_C

deleted def polynomial.derivative_hom

deleted def polynomial.derivative_lhom

deleted theorem polynomial.derivative_map

deleted theorem polynomial.derivative_monomial

deleted theorem polynomial.derivative_mul

deleted theorem polynomial.derivative_neg

deleted theorem polynomial.derivative_one

deleted theorem polynomial.derivative_pow

deleted theorem polynomial.derivative_pow_succ

deleted theorem polynomial.derivative_smul

deleted theorem polynomial.derivative_sub

deleted theorem polynomial.derivative_sum

deleted theorem polynomial.derivative_zero

deleted def polynomial.div

deleted def polynomial.div_X

deleted theorem polynomial.div_X_C

deleted theorem polynomial.div_X_add

deleted theorem polynomial.div_X_eq_zero_iff

deleted theorem polynomial.div_X_mul_X_add

deleted def polynomial.div_by_monic

deleted theorem polynomial.div_by_monic_eq_div

deleted theorem polynomial.div_by_monic_eq_of_not_monic

deleted theorem polynomial.div_by_monic_eq_zero_iff

deleted theorem polynomial.div_by_monic_mul_pow_root_multiplicity_eq

deleted theorem polynomial.div_by_monic_one

deleted theorem polynomial.div_by_monic_zero

deleted theorem polynomial.div_def

deleted theorem polynomial.div_eq_zero_iff

deleted theorem polynomial.div_mod_by_monic_unique

deleted theorem polynomial.div_wf_lemma

deleted theorem polynomial.dvd_iff_is_root

deleted theorem polynomial.dvd_iff_mod_by_monic_eq_zero

deleted theorem polynomial.dvd_term_of_dvd_eval_of_dvd_terms

deleted theorem polynomial.dvd_term_of_is_root_of_dvd_terms

deleted theorem polynomial.eq_C_of_degree_eq_zero

deleted theorem polynomial.eq_C_of_degree_le_zero

deleted theorem polynomial.eq_C_of_nat_degree_le_zero

deleted theorem polynomial.eq_X_add_C_of_degree_eq_one

deleted theorem polynomial.eq_X_add_C_of_degree_le_one

deleted theorem polynomial.eq_one_of_is_unit_of_monic

deleted theorem polynomial.eq_zero_of_eq_zero

deleted def polynomial.eval

deleted theorem polynomial.eval_C

deleted theorem polynomial.eval_X

deleted theorem polynomial.eval_add

deleted theorem polynomial.eval_bit0

deleted theorem polynomial.eval_bit1

deleted theorem polynomial.eval_comp

deleted theorem polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero

deleted theorem polynomial.eval_int_cast

deleted theorem polynomial.eval_map

deleted theorem polynomial.eval_monomial

deleted theorem polynomial.eval_mul

deleted theorem polynomial.eval_mul_X_sub_C

deleted theorem polynomial.eval_nat_cast

deleted theorem polynomial.eval_neg

deleted theorem polynomial.eval_one

deleted theorem polynomial.eval_pow

deleted theorem polynomial.eval_smul

deleted theorem polynomial.eval_sub

deleted def polynomial.eval_sub_factor

deleted theorem polynomial.eval_sum

deleted theorem polynomial.eval_unique

deleted theorem polynomial.eval_zero

deleted def polynomial.eval₂

deleted theorem polynomial.eval₂_C

deleted theorem polynomial.eval₂_X

deleted theorem polynomial.eval₂_X_pow

deleted theorem polynomial.eval₂_add

deleted theorem polynomial.eval₂_algebra_map_X

deleted theorem polynomial.eval₂_algebra_map_int_X

deleted theorem polynomial.eval₂_bit0

deleted theorem polynomial.eval₂_bit1

deleted theorem polynomial.eval₂_comp

deleted theorem polynomial.eval₂_eq_eval_map

deleted theorem polynomial.eval₂_hom

deleted theorem polynomial.eval₂_map

deleted theorem polynomial.eval₂_monomial

deleted theorem polynomial.eval₂_mul

deleted theorem polynomial.eval₂_nat_cast

deleted theorem polynomial.eval₂_neg

deleted theorem polynomial.eval₂_one

deleted theorem polynomial.eval₂_pow

deleted def polynomial.eval₂_ring_hom

deleted theorem polynomial.eval₂_smul

deleted theorem polynomial.eval₂_sub

deleted theorem polynomial.eval₂_sum

deleted theorem polynomial.eval₂_zero

deleted theorem polynomial.exists_finset_roots

deleted theorem polynomial.exists_root_of_degree_eq_one

deleted theorem polynomial.ext

deleted theorem polynomial.ext_iff

deleted theorem polynomial.finset_sum_coeff

deleted theorem polynomial.hom_eval₂

deleted theorem polynomial.integral_normalization_aeval_eq_zero

deleted theorem polynomial.integral_normalization_coeff_degree

deleted theorem polynomial.integral_normalization_coeff_nat_degree

deleted theorem polynomial.integral_normalization_coeff_ne_degree

deleted theorem polynomial.integral_normalization_coeff_ne_nat_degree

deleted theorem polynomial.integral_normalization_eval₂_eq_zero

deleted theorem polynomial.irreducible_X

deleted theorem polynomial.irreducible_X_sub_C

deleted theorem polynomial.irreducible_of_degree_eq_one

deleted theorem polynomial.irreducible_of_degree_eq_one_of_monic

deleted theorem polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero

deleted theorem polynomial.is_root.def

deleted def polynomial.is_root

deleted theorem polynomial.is_root_of_aeval_algebra_map_eq_zero

deleted theorem polynomial.is_root_of_eval₂_map_eq_zero

deleted theorem polynomial.is_unit_C

deleted theorem polynomial.is_unit_iff

deleted theorem polynomial.is_unit_iff_degree_eq_zero

deleted theorem polynomial.ite_le_nat_degree_coeff

deleted def polynomial.lcoeff

deleted theorem polynomial.lcoeff_apply

deleted theorem polynomial.le_degree_of_ne_zero

deleted theorem polynomial.le_nat_degree_of_ne_zero

deleted def polynomial.leading_coeff

deleted theorem polynomial.leading_coeff_C

deleted theorem polynomial.leading_coeff_X

deleted theorem polynomial.leading_coeff_X_pow

deleted theorem polynomial.leading_coeff_add_of_degree_eq

deleted theorem polynomial.leading_coeff_add_of_degree_lt

deleted theorem polynomial.leading_coeff_comp

deleted theorem polynomial.leading_coeff_eq_zero

deleted theorem polynomial.leading_coeff_eq_zero_iff_deg_eq_bot

deleted theorem polynomial.leading_coeff_map

deleted theorem polynomial.leading_coeff_monomial

deleted theorem polynomial.leading_coeff_mul'

deleted theorem polynomial.leading_coeff_mul

deleted theorem polynomial.leading_coeff_mul_X_pow

deleted theorem polynomial.leading_coeff_of_injective

deleted theorem polynomial.leading_coeff_one

deleted theorem polynomial.leading_coeff_pow'

deleted theorem polynomial.leading_coeff_pow

deleted theorem polynomial.leading_coeff_zero

deleted def polynomial.map

deleted theorem polynomial.map_C

deleted theorem polynomial.map_X

deleted theorem polynomial.map_add

deleted theorem polynomial.map_div

deleted theorem polynomial.map_div_by_monic

deleted theorem polynomial.map_eq_zero

deleted theorem polynomial.map_id

deleted theorem polynomial.map_injective

deleted theorem polynomial.map_map

deleted theorem polynomial.map_mod

deleted theorem polynomial.map_mod_by_monic

deleted theorem polynomial.map_mod_div_by_monic

deleted theorem polynomial.map_monomial

deleted theorem polynomial.map_mul

deleted theorem polynomial.map_nat_cast

deleted theorem polynomial.map_neg

deleted theorem polynomial.map_one

deleted theorem polynomial.map_pow

deleted theorem polynomial.map_sub

deleted theorem polynomial.map_zero

deleted theorem polynomial.mem_map_range

deleted theorem polynomial.mem_nth_roots

deleted theorem polynomial.mem_roots

deleted theorem polynomial.mem_roots_sub_C

deleted theorem polynomial.mem_support_derivative

deleted def polynomial.mod

deleted theorem polynomial.mod_X_sub_C_eq_C_eval

deleted def polynomial.mod_by_monic

deleted theorem polynomial.mod_by_monic_X

deleted theorem polynomial.mod_by_monic_X_sub_C_eq_C_eval

deleted theorem polynomial.mod_by_monic_add_div

deleted theorem polynomial.mod_by_monic_eq_mod

deleted theorem polynomial.mod_by_monic_eq_of_not_monic

deleted theorem polynomial.mod_by_monic_eq_self_iff

deleted theorem polynomial.mod_by_monic_eq_sub_mul_div

deleted theorem polynomial.mod_by_monic_one

deleted theorem polynomial.mod_by_monic_zero

deleted theorem polynomial.mod_def

deleted theorem polynomial.mod_eq_self_iff

deleted theorem polynomial.monic.as_sum

deleted theorem polynomial.monic.def

deleted theorem polynomial.monic.leading_coeff

deleted theorem polynomial.monic.ne_zero

deleted theorem polynomial.monic.ne_zero_of_zero_ne_one

deleted def polynomial.monic

deleted theorem polynomial.monic_X

deleted theorem polynomial.monic_X_add_C

deleted theorem polynomial.monic_X_pow_add

deleted theorem polynomial.monic_X_pow_sub

deleted theorem polynomial.monic_X_sub_C

deleted theorem polynomial.monic_integral_normalization

deleted theorem polynomial.monic_map

deleted theorem polynomial.monic_mul

deleted theorem polynomial.monic_mul_leading_coeff_inv

deleted theorem polynomial.monic_normalize

deleted theorem polynomial.monic_of_degree_le

deleted theorem polynomial.monic_of_injective

deleted theorem polynomial.monic_one

deleted theorem polynomial.monic_pow

deleted def polynomial.monomial

deleted theorem polynomial.monomial_add

deleted theorem polynomial.monomial_eq_smul_X

deleted theorem polynomial.monomial_one_eq_X_pow

deleted theorem polynomial.monomial_zero_left

deleted theorem polynomial.monomial_zero_right

deleted theorem polynomial.mul_X_pow_eq_zero

deleted theorem polynomial.mul_coeff_zero

deleted theorem polynomial.mul_comp

deleted theorem polynomial.mul_div_by_monic_eq_iff_is_root

deleted theorem polynomial.mul_div_eq_iff_is_root

deleted theorem polynomial.multiplicity_X_sub_C_finite

deleted theorem polynomial.multiplicity_finite_of_degree_pos_of_monic

deleted def polynomial.nat_degree

deleted theorem polynomial.nat_degree_C

deleted theorem polynomial.nat_degree_X

deleted theorem polynomial.nat_degree_X_le

deleted theorem polynomial.nat_degree_X_pow_sub_C

deleted theorem polynomial.nat_degree_X_sub_C

deleted theorem polynomial.nat_degree_X_sub_C_le

deleted theorem polynomial.nat_degree_coe_units

deleted theorem polynomial.nat_degree_comp

deleted theorem polynomial.nat_degree_comp_le

deleted theorem polynomial.nat_degree_derivative_lt

deleted theorem polynomial.nat_degree_div_by_monic

deleted theorem polynomial.nat_degree_eq_of_degree_eq

deleted theorem polynomial.nat_degree_eq_of_degree_eq_some

deleted theorem polynomial.nat_degree_eq_zero_iff_degree_le_zero

deleted theorem polynomial.nat_degree_int_cast

deleted theorem polynomial.nat_degree_le_nat_degree

deleted theorem polynomial.nat_degree_le_of_degree_le

deleted theorem polynomial.nat_degree_le_of_dvd

deleted theorem polynomial.nat_degree_map'

deleted theorem polynomial.nat_degree_map

deleted theorem polynomial.nat_degree_mul_eq'

deleted theorem polynomial.nat_degree_mul_eq

deleted theorem polynomial.nat_degree_mul_le

deleted theorem polynomial.nat_degree_nat_cast

deleted theorem polynomial.nat_degree_neg

deleted theorem polynomial.nat_degree_one

deleted theorem polynomial.nat_degree_pos_iff_degree_pos

deleted theorem polynomial.nat_degree_pos_of_aeval_root

deleted theorem polynomial.nat_degree_pos_of_eval₂_root

deleted theorem polynomial.nat_degree_pow_eq'

deleted theorem polynomial.nat_degree_pow_eq

deleted theorem polynomial.nat_degree_zero

deleted theorem polynomial.ne_zero_of_degree_gt

deleted theorem polynomial.ne_zero_of_monic

deleted theorem polynomial.ne_zero_of_monic_of_zero_ne_one

deleted theorem polynomial.ne_zero_of_ne_zero_of_monic

deleted theorem polynomial.nonzero.of_polynomial_ne

deleted theorem polynomial.not_is_unit_X

deleted theorem polynomial.not_is_unit_X_sub_C

deleted theorem polynomial.not_monic_zero

deleted def polynomial.nth_roots

deleted theorem polynomial.of_mem_support_derivative

deleted theorem polynomial.one_comp

deleted theorem polynomial.pairwise_coprime_X_sub

deleted def polynomial.pow_add_expansion

deleted theorem polynomial.pow_root_multiplicity_dvd

deleted def polynomial.pow_sub_pow_factor

deleted theorem polynomial.prime_X

deleted theorem polynomial.prime_X_sub_C

deleted theorem polynomial.prime_of_degree_eq_one

deleted theorem polynomial.prime_of_degree_eq_one_of_monic

deleted theorem polynomial.ring_hom_eval₂_algebra_map_int

deleted theorem polynomial.root_X_sub_C

deleted theorem polynomial.root_mul

deleted theorem polynomial.root_mul_left_of_is_root

deleted theorem polynomial.root_mul_right_of_is_root

deleted def polynomial.root_multiplicity

deleted theorem polynomial.root_multiplicity_eq_multiplicity

deleted theorem polynomial.root_or_root_of_root_mul

deleted theorem polynomial.roots_X_sub_C

deleted theorem polynomial.roots_mul

deleted theorem polynomial.single_eq_C_mul_X

deleted theorem polynomial.subsingleton_of_monic_zero

deleted theorem polynomial.sum_C_index

deleted theorem polynomial.sum_C_mul_X_eq

deleted theorem polynomial.sum_monomial_eq

deleted theorem polynomial.sum_over_range'

deleted theorem polynomial.sum_over_range

deleted theorem polynomial.support_integral_normalization

deleted theorem polynomial.support_zero

deleted theorem polynomial.zero_comp

deleted theorem polynomial.zero_div_by_monic

deleted theorem polynomial.zero_is_root_of_coeff_zero_eq_zero

deleted theorem polynomial.zero_le_degree_iff

deleted theorem polynomial.zero_mod_by_monic

deleted def polynomial

Created src/data/polynomial/algebra_map.lean

added theorem polynomial.C_eq_algebra_map

added theorem polynomial.C_inj

added theorem polynomial.C_mul'

added def polynomial.aeval

added theorem polynomial.aeval_C

added theorem polynomial.aeval_X

added theorem polynomial.aeval_alg_hom

added theorem polynomial.aeval_alg_hom_apply

added theorem polynomial.aeval_def

added theorem polynomial.alg_hom_eval₂_algebra_map

added theorem polynomial.algebra_map_apply

added theorem polynomial.dvd_term_of_dvd_eval_of_dvd_terms

added theorem polynomial.dvd_term_of_is_root_of_dvd_terms

added theorem polynomial.eval_comp

added theorem polynomial.eval_mul

added theorem polynomial.eval_mul_X_sub_C

added theorem polynomial.eval_pow

added theorem polynomial.eval_unique

added theorem polynomial.eval₂_algebra_map_X

added theorem polynomial.eval₂_algebra_map_int_X

added theorem polynomial.eval₂_comp

added theorem polynomial.eval₂_hom

added theorem polynomial.is_root_of_aeval_algebra_map_eq_zero

added theorem polynomial.is_root_of_eval₂_map_eq_zero

added theorem polynomial.mul_comp

added theorem polynomial.not_is_unit_X_sub_C

added theorem polynomial.ring_hom_eval₂_algebra_map_int

added theorem polynomial.root_mul_left_of_is_root

added theorem polynomial.root_mul_right_of_is_root

Created src/data/polynomial/basic.lean

added def polynomial.X

added theorem polynomial.X_mul

added theorem polynomial.X_pow_mul

added theorem polynomial.X_pow_mul_assoc

added theorem polynomial.apply_eq_coeff

added def polynomial.coeff

added def polynomial.coeff_coe_to_fun

added theorem polynomial.coeff_mk

added theorem polynomial.coeff_neg

added theorem polynomial.coeff_one_zero

added theorem polynomial.coeff_single

added theorem polynomial.coeff_sub

added theorem polynomial.coeff_zero

added theorem polynomial.eq_zero_of_eq_zero

added theorem polynomial.ext

added theorem polynomial.ext_iff

added def polynomial.monomial

added theorem polynomial.monomial_add

added theorem polynomial.monomial_zero_right

added theorem polynomial.support_zero

added def polynomial

Created src/data/polynomial/coeff.lean

added theorem polynomial.coeff_C_mul

added theorem polynomial.coeff_C_mul_X

added theorem polynomial.coeff_X_pow

added theorem polynomial.coeff_add

added theorem polynomial.coeff_mul

added theorem polynomial.coeff_mul_C

added theorem polynomial.coeff_mul_X

added theorem polynomial.coeff_mul_X_pow

added theorem polynomial.coeff_mul_X_zero

added theorem polynomial.coeff_one

added theorem polynomial.coeff_smul

added theorem polynomial.coeff_sum

added def polynomial.lcoeff

added theorem polynomial.lcoeff_apply

added theorem polynomial.monomial_eq_smul_X

added theorem polynomial.monomial_one_eq_X_pow

added theorem polynomial.mul_X_pow_eq_zero

added theorem polynomial.mul_coeff_zero

Created src/data/polynomial/default.lean

Created src/data/polynomial/degree.lean

added theorem polynomial.X_pow_sub_C_ne_zero

added theorem polynomial.X_sub_C_ne_zero

added theorem polynomial.coeff_mul_degree_add_degree

added theorem polynomial.coeff_nat_degree_eq_zero_of_degree_lt

added theorem polynomial.degree_X_pow

added theorem polynomial.degree_X_pow_sub_C

added theorem polynomial.degree_X_sub_C

added theorem polynomial.degree_add_C

added theorem polynomial.degree_add_eq_of_degree_lt

added theorem polynomial.degree_add_eq_of_leading_coeff_add_ne_zero

added theorem polynomial.degree_add_le

added theorem polynomial.degree_erase_le

added theorem polynomial.degree_erase_lt

added theorem polynomial.degree_le_iff_coeff_zero

added theorem polynomial.degree_le_zero_iff

added theorem polynomial.degree_lt_degree_mul_X

added theorem polynomial.degree_map'

added theorem polynomial.degree_map_eq_of_injective

added theorem polynomial.degree_map_eq_of_leading_coeff_ne_zero

added theorem polynomial.degree_map_le

added theorem polynomial.degree_mul_eq'

added theorem polynomial.degree_mul_le

added theorem polynomial.degree_nonneg_iff_ne_zero

added theorem polynomial.degree_pos_of_eval₂_root

added theorem polynomial.degree_pos_of_root

added theorem polynomial.degree_pow_eq'

added theorem polynomial.degree_pow_le

added theorem polynomial.degree_sub_le

added theorem polynomial.degree_sub_lt

added theorem polynomial.degree_sum_le

added theorem polynomial.eq_C_of_degree_eq_zero

added theorem polynomial.eq_C_of_degree_le_zero

added theorem polynomial.eq_C_of_nat_degree_le_zero

added theorem polynomial.leading_coeff_C

added theorem polynomial.leading_coeff_X

added theorem polynomial.leading_coeff_X_pow

added theorem polynomial.leading_coeff_add_of_degree_eq

added theorem polynomial.leading_coeff_add_of_degree_lt

added theorem polynomial.leading_coeff_eq_zero

added theorem polynomial.leading_coeff_eq_zero_iff_deg_eq_bot

added theorem polynomial.leading_coeff_monomial

added theorem polynomial.leading_coeff_mul'

added theorem polynomial.leading_coeff_mul_X_pow

added theorem polynomial.leading_coeff_one

added theorem polynomial.leading_coeff_pow'

added theorem polynomial.leading_coeff_zero

added theorem polynomial.monic.ne_zero

added theorem polynomial.monic.ne_zero_of_zero_ne_one

added theorem polynomial.monic_X

added theorem polynomial.monic_one

added theorem polynomial.nat_degree_X_pow_sub_C

added theorem polynomial.nat_degree_X_sub_C

added theorem polynomial.nat_degree_X_sub_C_le

added theorem polynomial.nat_degree_comp_le

added theorem polynomial.nat_degree_eq_zero_iff_degree_le_zero

added theorem polynomial.nat_degree_map'

added theorem polynomial.nat_degree_mul_eq'

added theorem polynomial.nat_degree_mul_le

added theorem polynomial.nat_degree_pos_iff_degree_pos

added theorem polynomial.nat_degree_pos_of_eval₂_root

added theorem polynomial.nat_degree_pow_eq'

added theorem polynomial.ne_zero_of_degree_gt

added theorem polynomial.not_is_unit_X

added theorem polynomial.subsingleton_of_monic_zero

added theorem polynomial.zero_le_degree_iff

Created src/data/polynomial/degree/basic.lean

added theorem polynomial.C_eq_int_cast

added theorem polynomial.coeff_eq_zero_of_degree_lt

added theorem polynomial.coeff_eq_zero_of_nat_degree_lt

added theorem polynomial.coeff_mul_X_sub_C

added theorem polynomial.coeff_nat_degree_succ_eq_zero

added theorem polynomial.coeff_ne_zero_of_eq_degree

added def polynomial.degree

added theorem polynomial.degree_C

added theorem polynomial.degree_C_le

added theorem polynomial.degree_C_mul_X_pow_le

added theorem polynomial.degree_X

added theorem polynomial.degree_X_le

added theorem polynomial.degree_X_pow_le

added theorem polynomial.degree_eq_bot

added theorem polynomial.degree_eq_iff_nat_degree_eq

added theorem polynomial.degree_eq_iff_nat_degree_eq_of_pos

added theorem polynomial.degree_eq_nat_degree

added theorem polynomial.degree_le_degree

added theorem polynomial.degree_le_nat_degree

added theorem polynomial.degree_lt_wf

added theorem polynomial.degree_monomial

added theorem polynomial.degree_monomial_le

added theorem polynomial.degree_ne_of_nat_degree_ne

added theorem polynomial.degree_neg

added theorem polynomial.degree_one

added theorem polynomial.degree_one_le

added theorem polynomial.degree_zero

added theorem polynomial.eq_X_add_C_of_degree_eq_one

added theorem polynomial.eq_X_add_C_of_degree_le_one

added theorem polynomial.ite_le_nat_degree_coeff

added theorem polynomial.le_degree_of_ne_zero

added theorem polynomial.le_nat_degree_of_ne_zero

added def polynomial.leading_coeff

added theorem polynomial.monic.def

added theorem polynomial.monic.leading_coeff

added def polynomial.monic

added def polynomial.nat_degree

added theorem polynomial.nat_degree_C

added theorem polynomial.nat_degree_X

added theorem polynomial.nat_degree_X_le

added theorem polynomial.nat_degree_eq_of_degree_eq

added theorem polynomial.nat_degree_eq_of_degree_eq_some

added theorem polynomial.nat_degree_int_cast

added theorem polynomial.nat_degree_le_nat_degree

added theorem polynomial.nat_degree_le_of_degree_le

added theorem polynomial.nat_degree_nat_cast

added theorem polynomial.nat_degree_neg

added theorem polynomial.nat_degree_one

added theorem polynomial.nat_degree_zero

Created src/data/polynomial/derivative.lean

added theorem polynomial.coeff_derivative

added theorem polynomial.degree_derivative_eq

added theorem polynomial.degree_derivative_le

added theorem polynomial.degree_derivative_lt

added def polynomial.derivative

added theorem polynomial.derivative_C

added theorem polynomial.derivative_X

added theorem polynomial.derivative_add

added theorem polynomial.derivative_eval

added theorem polynomial.derivative_eval₂_C

added def polynomial.derivative_hom

added def polynomial.derivative_lhom

added theorem polynomial.derivative_map

added theorem polynomial.derivative_monomial

added theorem polynomial.derivative_mul

added theorem polynomial.derivative_neg

added theorem polynomial.derivative_one

added theorem polynomial.derivative_pow

added theorem polynomial.derivative_pow_succ

added theorem polynomial.derivative_smul

added theorem polynomial.derivative_sub

added theorem polynomial.derivative_sum

added theorem polynomial.derivative_zero

added theorem polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero

added theorem polynomial.mem_support_derivative

added theorem polynomial.nat_degree_derivative_lt

added theorem polynomial.of_mem_support_derivative

Created src/data/polynomial/div.lean

added theorem polynomial.X_dvd_iff

added def polynomial.decidable_dvd_monic

added theorem polynomial.degree_add_div_by_monic

added theorem polynomial.degree_div_X_lt

added theorem polynomial.degree_div_by_monic_le

added theorem polynomial.degree_div_by_monic_lt

added theorem polynomial.degree_mod_by_monic_le

added theorem polynomial.degree_mod_by_monic_lt

added theorem polynomial.degree_pos_induction_on

added def polynomial.div_X

added theorem polynomial.div_X_C

added theorem polynomial.div_X_add

added theorem polynomial.div_X_eq_zero_iff

added theorem polynomial.div_X_mul_X_add

added def polynomial.div_by_monic

added theorem polynomial.div_by_monic_eq_of_not_monic

added theorem polynomial.div_by_monic_eq_zero_iff

added theorem polynomial.div_by_monic_mul_pow_root_multiplicity_eq

added theorem polynomial.div_by_monic_one

added theorem polynomial.div_by_monic_zero

added theorem polynomial.div_mod_by_monic_unique

added theorem polynomial.div_wf_lemma

added theorem polynomial.dvd_iff_is_root

added theorem polynomial.dvd_iff_mod_by_monic_eq_zero

added theorem polynomial.eval_div_by_monic_pow_root_multiplicity_ne_zero

added theorem polynomial.map_div_by_monic

added theorem polynomial.map_mod_by_monic

added theorem polynomial.map_mod_div_by_monic

added def polynomial.mod_by_monic

added theorem polynomial.mod_by_monic_X

added theorem polynomial.mod_by_monic_X_sub_C_eq_C_eval

added theorem polynomial.mod_by_monic_add_div

added theorem polynomial.mod_by_monic_eq_of_not_monic

added theorem polynomial.mod_by_monic_eq_self_iff

added theorem polynomial.mod_by_monic_eq_sub_mul_div

added theorem polynomial.mod_by_monic_one

added theorem polynomial.mod_by_monic_zero

added theorem polynomial.mul_div_by_monic_eq_iff_is_root

added theorem polynomial.multiplicity_X_sub_C_finite

added theorem polynomial.multiplicity_finite_of_degree_pos_of_monic

added theorem polynomial.nat_degree_div_by_monic

added theorem polynomial.pow_root_multiplicity_dvd

added def polynomial.root_multiplicity

added theorem polynomial.root_multiplicity_eq_multiplicity

added theorem polynomial.zero_div_by_monic

added theorem polynomial.zero_mod_by_monic

Created src/data/polynomial/eval.lean

added theorem polynomial.C_comp

added theorem polynomial.C_neg

added theorem polynomial.C_sub

added theorem polynomial.X_comp

added theorem polynomial.add_comp

added theorem polynomial.coe_eval₂_ring_hom

added theorem polynomial.coeff_map

added theorem polynomial.coeff_zero_eq_eval_zero

added def polynomial.comp

added theorem polynomial.comp_C

added theorem polynomial.comp_X

added theorem polynomial.comp_one

added theorem polynomial.comp_zero

added def polynomial.eval

added theorem polynomial.eval_C

added theorem polynomial.eval_X

added theorem polynomial.eval_add

added theorem polynomial.eval_bit0

added theorem polynomial.eval_bit1

added theorem polynomial.eval_int_cast

added theorem polynomial.eval_map

added theorem polynomial.eval_monomial

added theorem polynomial.eval_nat_cast

added theorem polynomial.eval_neg

added theorem polynomial.eval_one

added theorem polynomial.eval_smul

added theorem polynomial.eval_sub

added theorem polynomial.eval_sum

added theorem polynomial.eval_zero

added def polynomial.eval₂

added theorem polynomial.eval₂_C

added theorem polynomial.eval₂_X

added theorem polynomial.eval₂_X_pow

added theorem polynomial.eval₂_add

added theorem polynomial.eval₂_bit0

added theorem polynomial.eval₂_bit1

added theorem polynomial.eval₂_eq_eval_map

added theorem polynomial.eval₂_finset_sum

added theorem polynomial.eval₂_map

added theorem polynomial.eval₂_monomial

added theorem polynomial.eval₂_mul

added theorem polynomial.eval₂_nat_cast

added theorem polynomial.eval₂_neg

added theorem polynomial.eval₂_one

added theorem polynomial.eval₂_pow

added def polynomial.eval₂_ring_hom

added theorem polynomial.eval₂_smul

added theorem polynomial.eval₂_sub

added theorem polynomial.eval₂_sum

added theorem polynomial.eval₂_zero

added theorem polynomial.hom_eval₂

added theorem polynomial.is_root.def

added def polynomial.is_root

added def polynomial.map

added theorem polynomial.map_C

added theorem polynomial.map_X

added theorem polynomial.map_add

added theorem polynomial.map_id

added theorem polynomial.map_injective

added theorem polynomial.map_map

added theorem polynomial.map_monomial

added theorem polynomial.map_mul

added theorem polynomial.map_nat_cast

added theorem polynomial.map_neg

added theorem polynomial.map_one

added theorem polynomial.map_pow

added theorem polynomial.map_sub

added theorem polynomial.map_zero

added theorem polynomial.mem_map_range

added theorem polynomial.one_comp

added theorem polynomial.root_X_sub_C

added theorem polynomial.zero_comp

added theorem polynomial.zero_is_root_of_coeff_zero_eq_zero

Created src/data/polynomial/field_division.lean

added theorem polynomial.coe_norm_unit

added theorem polynomial.coeff_inv_units

added theorem polynomial.degree_add_div

added theorem polynomial.degree_div_le

added theorem polynomial.degree_div_lt

added theorem polynomial.degree_map

added theorem polynomial.degree_mul_leading_coeff_inv

added theorem polynomial.degree_normalize

added theorem polynomial.degree_pos_of_ne_zero_of_nonunit

added def polynomial.div

added theorem polynomial.div_by_monic_eq_div

added theorem polynomial.div_def

added theorem polynomial.div_eq_zero_iff

added theorem polynomial.exists_root_of_degree_eq_one

added theorem polynomial.irreducible_of_degree_eq_one

added theorem polynomial.is_unit_iff_degree_eq_zero

added theorem polynomial.leading_coeff_map

added theorem polynomial.map_div

added theorem polynomial.map_eq_zero

added theorem polynomial.map_mod

added def polynomial.mod

added theorem polynomial.mod_X_sub_C_eq_C_eval

added theorem polynomial.mod_by_monic_eq_mod

added theorem polynomial.mod_def

added theorem polynomial.mod_eq_self_iff

added theorem polynomial.monic_mul_leading_coeff_inv

added theorem polynomial.monic_normalize

added theorem polynomial.mul_div_eq_iff_is_root

added theorem polynomial.nat_degree_map

added theorem polynomial.pairwise_coprime_X_sub

added theorem polynomial.prime_of_degree_eq_one

Created src/data/polynomial/identities.lean

added def polynomial.binom_expansion

added def polynomial.eval_sub_factor

added def polynomial.pow_add_expansion

added def polynomial.pow_sub_pow_factor

Created src/data/polynomial/induction.lean

added theorem polynomial.as_sum

added theorem polynomial.coeff_monomial_mul

added theorem polynomial.coeff_monomial_zero_mul

added theorem polynomial.coeff_mul_monomial

added theorem polynomial.coeff_mul_monomial_zero

added theorem polynomial.finset_sum_coeff

added theorem polynomial.sum_C_mul_X_eq

added theorem polynomial.sum_monomial_eq

added theorem polynomial.sum_over_range'

added theorem polynomial.sum_over_range

Created src/data/polynomial/monic.lean

added theorem polynomial.eq_one_of_is_unit_of_monic

added theorem polynomial.integral_normalization_aeval_eq_zero

added theorem polynomial.integral_normalization_coeff_degree

added theorem polynomial.integral_normalization_coeff_nat_degree

added theorem polynomial.integral_normalization_coeff_ne_degree

added theorem polynomial.integral_normalization_coeff_ne_nat_degree

added theorem polynomial.integral_normalization_eval₂_eq_zero

added theorem polynomial.is_unit_C

added theorem polynomial.leading_coeff_of_injective

added theorem polynomial.monic.as_sum

added theorem polynomial.monic_X_add_C

added theorem polynomial.monic_X_pow_add

added theorem polynomial.monic_X_pow_sub

added theorem polynomial.monic_X_sub_C

added theorem polynomial.monic_integral_normalization

added theorem polynomial.monic_map

added theorem polynomial.monic_mul

added theorem polynomial.monic_of_degree_le

added theorem polynomial.monic_of_injective

added theorem polynomial.monic_pow

added theorem polynomial.ne_zero_of_monic

added theorem polynomial.ne_zero_of_monic_of_zero_ne_one

added theorem polynomial.ne_zero_of_ne_zero_of_monic

added theorem polynomial.not_monic_zero

added theorem polynomial.support_integral_normalization

Created src/data/polynomial/monomial.lean

added def polynomial.C

added theorem polynomial.C_0

added theorem polynomial.C_1

added theorem polynomial.C_add

added theorem polynomial.C_bit0

added theorem polynomial.C_bit1

added theorem polynomial.C_eq_nat_cast

added theorem polynomial.C_mul

added theorem polynomial.C_pow

added theorem polynomial.X_ne_zero

added theorem polynomial.coeff_C

added theorem polynomial.coeff_C_zero

added theorem polynomial.coeff_X

added theorem polynomial.coeff_X_one

added theorem polynomial.coeff_X_zero

added theorem polynomial.monomial_zero_left

added theorem polynomial.nonzero.of_polynomial_ne

added theorem polynomial.single_eq_C_mul_X

added theorem polynomial.sum_C_index

Created src/data/polynomial/ring_division.lean

added theorem is_integral_domain.polynomial

added theorem polynomial.card_nth_roots

added theorem polynomial.card_roots'

added theorem polynomial.card_roots

added theorem polynomial.card_roots_X_pow_sub_C

added theorem polynomial.card_roots_sub_C'

added theorem polynomial.card_roots_sub_C

added theorem polynomial.coeff_coe_units_zero_ne_zero

added theorem polynomial.coeff_comp_degree_mul_degree

added theorem polynomial.degree_coe_units

added theorem polynomial.degree_eq_degree_of_associated

added theorem polynomial.degree_eq_one_of_irreducible_of_root

added theorem polynomial.degree_eq_zero_of_is_unit

added theorem polynomial.degree_le_mul_left

added theorem polynomial.degree_mul_eq

added theorem polynomial.degree_pos_of_aeval_root

added theorem polynomial.degree_pow_eq

added theorem polynomial.exists_finset_roots

added theorem polynomial.irreducible_X

added theorem polynomial.irreducible_X_sub_C

added theorem polynomial.irreducible_of_degree_eq_one_of_monic

added theorem polynomial.is_unit_iff

added theorem polynomial.leading_coeff_comp

added theorem polynomial.leading_coeff_mul

added theorem polynomial.leading_coeff_pow

added theorem polynomial.mem_nth_roots

added theorem polynomial.mem_roots

added theorem polynomial.mem_roots_sub_C

added theorem polynomial.nat_degree_coe_units

added theorem polynomial.nat_degree_comp

added theorem polynomial.nat_degree_le_of_dvd

added theorem polynomial.nat_degree_mul_eq

added theorem polynomial.nat_degree_pos_of_aeval_root

added theorem polynomial.nat_degree_pow_eq

added def polynomial.nth_roots

added theorem polynomial.prime_X

added theorem polynomial.prime_X_sub_C

added theorem polynomial.prime_of_degree_eq_one_of_monic

added theorem polynomial.root_mul

added theorem polynomial.root_or_root_of_root_mul

added theorem polynomial.roots_X_sub_C

added theorem polynomial.roots_mul