Commit 2023-03-08 11:35 f71cc3ab

View on Github →

feat: port Data.Polynomial.Eval (#2645)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.C_comp

added theorem Polynomial.C_mul_comp

added theorem Polynomial.C_neg

added theorem Polynomial.C_sub

added theorem Polynomial.IsRoot.def

added theorem Polynomial.IsRoot.dvd

added theorem Polynomial.IsRoot.eq_zero

added theorem Polynomial.IsRoot.map

added theorem Polynomial.IsRoot.of_map

added def Polynomial.IsRoot

added theorem Polynomial.X_comp

added theorem Polynomial.X_pow_comp

added theorem Polynomial.add_comp

added theorem Polynomial.bit0_comp

added theorem Polynomial.bit1_comp

added theorem Polynomial.cast_int_comp

added theorem Polynomial.coe_compRingHom

added theorem Polynomial.coe_compRingHom_apply

added theorem Polynomial.coe_evalRingHom

added theorem Polynomial.coe_eval₂RingHom

added theorem Polynomial.coe_mapRingHom

added theorem Polynomial.coeff_comp_degree_mul_degree

added theorem Polynomial.coeff_map

added theorem Polynomial.coeff_zero_eq_eval_zero

added def Polynomial.comp

added def Polynomial.compRingHom

added theorem Polynomial.comp_C

added theorem Polynomial.comp_X

added theorem Polynomial.comp_assoc

added theorem Polynomial.comp_eq_sum_left

added theorem Polynomial.comp_one

added theorem Polynomial.comp_zero

added theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero

added theorem Polynomial.degree_map_le

added def Polynomial.eval

added def Polynomial.evalRingHom

added theorem Polynomial.evalRingHom_zero

added theorem Polynomial.eval_C

added theorem Polynomial.eval_C_mul

added theorem Polynomial.eval_X

added theorem Polynomial.eval_add

added theorem Polynomial.eval_bit0

added theorem Polynomial.eval_bit1

added theorem Polynomial.eval_comp

added theorem Polynomial.eval_dvd

added theorem Polynomial.eval_eq_sum

added theorem Polynomial.eval_eq_sum_range'

added theorem Polynomial.eval_eq_sum_range

added theorem Polynomial.eval_eq_zero_of_dvd_of_eval_eq_zero

added theorem Polynomial.eval_finset_sum

added theorem Polynomial.eval_geom_sum

added theorem Polynomial.eval_int_cast

added theorem Polynomial.eval_int_cast_map

added theorem Polynomial.eval_list_prod

added theorem Polynomial.eval_map

added theorem Polynomial.eval_monomial

added theorem Polynomial.eval_monomial_one_add_sub

added theorem Polynomial.eval_mul

added theorem Polynomial.eval_mul_X

added theorem Polynomial.eval_mul_X_pow

added theorem Polynomial.eval_multiset_prod

added theorem Polynomial.eval_nat_cast

added theorem Polynomial.eval_nat_cast_map

added theorem Polynomial.eval_nat_cast_mul

added theorem Polynomial.eval_neg

added theorem Polynomial.eval_one

added theorem Polynomial.eval_one_map

added theorem Polynomial.eval_pow

added theorem Polynomial.eval_prod

added theorem Polynomial.eval_smul

added theorem Polynomial.eval_sub

added theorem Polynomial.eval_sum

added theorem Polynomial.eval_surjective

added theorem Polynomial.eval_zero

added theorem Polynomial.eval_zero_map

added def Polynomial.eval₂AddMonoidHom

added def Polynomial.eval₂RingHom'

added def Polynomial.eval₂RingHom

added theorem Polynomial.eval₂_C

added theorem Polynomial.eval₂_C_X

added theorem Polynomial.eval₂_X

added theorem Polynomial.eval₂_X_mul

added theorem Polynomial.eval₂_X_pow

added theorem Polynomial.eval₂_add

added theorem Polynomial.eval₂_at_apply

added theorem Polynomial.eval₂_at_nat_cast

added theorem Polynomial.eval₂_at_one

added theorem Polynomial.eval₂_at_zero

added theorem Polynomial.eval₂_bit0

added theorem Polynomial.eval₂_bit1

added theorem Polynomial.eval₂_comp

added theorem Polynomial.eval₂_congr

added theorem Polynomial.eval₂_dvd

added theorem Polynomial.eval₂_eq_eval_map

added theorem Polynomial.eval₂_eq_sum

added theorem Polynomial.eval₂_eq_sum_range'

added theorem Polynomial.eval₂_eq_sum_range

added theorem Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero

added theorem Polynomial.eval₂_finset_prod

added theorem Polynomial.eval₂_finset_sum

added theorem Polynomial.eval₂_hom

added theorem Polynomial.eval₂_list_prod

added theorem Polynomial.eval₂_list_prod_noncomm

added theorem Polynomial.eval₂_list_sum

added theorem Polynomial.eval₂_map

added theorem Polynomial.eval₂_monomial

added theorem Polynomial.eval₂_mul

added theorem Polynomial.eval₂_mul_C'

added theorem Polynomial.eval₂_mul_X

added theorem Polynomial.eval₂_mul_eq_zero_of_left

added theorem Polynomial.eval₂_mul_eq_zero_of_right

added theorem Polynomial.eval₂_mul_noncomm

added theorem Polynomial.eval₂_multiset_prod

added theorem Polynomial.eval₂_multiset_sum

added theorem Polynomial.eval₂_nat_cast

added theorem Polynomial.eval₂_neg

added theorem Polynomial.eval₂_ofFinsupp

added theorem Polynomial.eval₂_one

added theorem Polynomial.eval₂_pow

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.isRoot_map_iff

added theorem Polynomial.isRoot_prod

added theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero

added def Polynomial.leval

added theorem Polynomial.list_prod_comp

added def Polynomial.map

added def Polynomial.mapEquiv

added def Polynomial.mapRingHom

added theorem Polynomial.mapRingHom_comp

added theorem Polynomial.mapRingHom_id

added theorem Polynomial.map_C

added theorem Polynomial.map_X

added theorem Polynomial.map_comp

added theorem Polynomial.map_dvd

added theorem Polynomial.map_id

added theorem Polynomial.map_injective

added theorem Polynomial.map_int_cast

added theorem Polynomial.map_map

added theorem Polynomial.map_monic_eq_zero_iff

added theorem Polynomial.map_monic_ne_zero

added theorem Polynomial.map_monomial

added theorem Polynomial.map_surjective

added theorem Polynomial.mem_map_range

added theorem Polynomial.mem_map_rangeS

added theorem Polynomial.monomial_comp

added theorem Polynomial.mul_X_comp

added theorem Polynomial.mul_X_pow_comp

added theorem Polynomial.mul_comp

added theorem Polynomial.multiset_prod_comp

added theorem Polynomial.natDegree_map_le

added theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero

added theorem Polynomial.nat_cast_comp

added theorem Polynomial.nat_cast_mul_comp

added theorem Polynomial.neg_comp

added theorem Polynomial.not_isRoot_C

added theorem Polynomial.one_comp

added theorem Polynomial.pow_comp

added theorem Polynomial.prod_comp

added theorem Polynomial.root_X_sub_C

added theorem Polynomial.root_mul_left_of_isRoot

added theorem Polynomial.root_mul_right_of_isRoot

added theorem Polynomial.smul_comp

added theorem Polynomial.sub_comp

added theorem Polynomial.support_map_of_injective

added theorem Polynomial.support_map_subset

added theorem Polynomial.zero_comp

added theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero