Commit 2023-03-08 07:29 301a5b54

View on Github →

feat: port Data.Polynomial.Basic (#2620)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Basic.lean

added theorem IsSMulRegular.polynomial

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_int_cast

added theorem Polynomial.C_eq_nat_cast

added theorem Polynomial.C_eq_zero

added theorem Polynomial.C_inj

added theorem Polynomial.C_injective

added theorem Polynomial.C_mul

added theorem Polynomial.C_mul_X_eq_monomial

added theorem Polynomial.C_mul_X_pow_eq_monomial

added theorem Polynomial.C_mul_monomial

added theorem Polynomial.C_ne_zero

added theorem Polynomial.C_pow

added theorem Polynomial.Nontrivial.of_polynomial_ne

added def Polynomial.X

added theorem Polynomial.X_mul

added theorem Polynomial.X_mul_C

added theorem Polynomial.X_mul_monomial

added theorem Polynomial.X_ne_zero

added theorem Polynomial.X_pow_eq_monomial

added theorem Polynomial.X_pow_mul

added theorem Polynomial.X_pow_mul_C

added theorem Polynomial.X_pow_mul_assoc

added theorem Polynomial.X_pow_mul_assoc_C

added theorem Polynomial.X_pow_mul_monomial

added theorem Polynomial.addHom_ext'

added theorem Polynomial.addHom_ext

added theorem Polynomial.addSubmonoid_closure_setOf_eq_monomial

added theorem Polynomial.binomial_eq_binomial

added theorem Polynomial.card_support_eq_zero

added def Polynomial.coeff

added theorem Polynomial.coeff_C

added theorem Polynomial.coeff_C_ne_zero

added theorem Polynomial.coeff_C_zero

added theorem Polynomial.coeff_X

added theorem Polynomial.coeff_X_of_ne_one

added theorem Polynomial.coeff_X_one

added theorem Polynomial.coeff_X_zero

added theorem Polynomial.coeff_erase

added theorem Polynomial.coeff_inj

added theorem Polynomial.coeff_injective

added theorem Polynomial.coeff_monomial

added theorem Polynomial.coeff_monomial_succ

added theorem Polynomial.coeff_neg

added theorem Polynomial.coeff_ofFinsupp

added theorem Polynomial.coeff_one_zero

added theorem Polynomial.coeff_sub

added theorem Polynomial.coeff_update

added theorem Polynomial.coeff_update_apply

added theorem Polynomial.coeff_update_ne

added theorem Polynomial.coeff_update_same

added theorem Polynomial.coeff_zero

added theorem Polynomial.commute_X

added theorem Polynomial.commute_X_pow

added theorem Polynomial.eq_zero_of_eq_zero

added theorem Polynomial.erase_monomial

added theorem Polynomial.erase_ne

added theorem Polynomial.erase_same

added theorem Polynomial.erase_zero

added theorem Polynomial.eta

added theorem Polynomial.exists_iff_exists_finsupp

added theorem Polynomial.ext

added theorem Polynomial.ext_iff

added theorem Polynomial.forall_eq_iff_forall_eq

added theorem Polynomial.forall_iff_forall_finsupp

added theorem Polynomial.lhom_ext'

added theorem Polynomial.mem_support_iff

added def Polynomial.monomial

added theorem Polynomial.monomial_add

added theorem Polynomial.monomial_add_erase

added theorem Polynomial.monomial_eq_zero_iff

added theorem Polynomial.monomial_injective

added theorem Polynomial.monomial_left_inj

added theorem Polynomial.monomial_mul_C

added theorem Polynomial.monomial_mul_X

added theorem Polynomial.monomial_mul_X_pow

added theorem Polynomial.monomial_mul_monomial

added theorem Polynomial.monomial_neg

added theorem Polynomial.monomial_one_one_eq_X

added theorem Polynomial.monomial_one_right_eq_X_pow

added theorem Polynomial.monomial_pow

added theorem Polynomial.monomial_zero_left

added theorem Polynomial.monomial_zero_one

added theorem Polynomial.monomial_zero_right

added theorem Polynomial.mul_eq_sum_sum

added theorem Polynomial.nat_cast_mul

added theorem Polynomial.nontrivial_iff

added theorem Polynomial.not_mem_support_iff

added theorem Polynomial.ofFinsupp_add

added theorem Polynomial.ofFinsupp_eq_one

added theorem Polynomial.ofFinsupp_eq_zero

added theorem Polynomial.ofFinsupp_erase

added theorem Polynomial.ofFinsupp_inj

added theorem Polynomial.ofFinsupp_mul

added theorem Polynomial.ofFinsupp_neg

added theorem Polynomial.ofFinsupp_one

added theorem Polynomial.ofFinsupp_pow

added theorem Polynomial.ofFinsupp_single

added theorem Polynomial.ofFinsupp_smul

added theorem Polynomial.ofFinsupp_sub

added theorem Polynomial.ofFinsupp_sum

added theorem Polynomial.ofFinsupp_zero

added theorem Polynomial.smul_C

added theorem Polynomial.smul_X_eq_monomial

added theorem Polynomial.smul_monomial

added theorem Polynomial.subsingleton_iff_subsingleton

added def Polynomial.sum

added theorem Polynomial.sum_C_index

added theorem Polynomial.sum_C_mul_X_pow_eq

added theorem Polynomial.sum_X_index

added theorem Polynomial.sum_add'

added theorem Polynomial.sum_add

added theorem Polynomial.sum_add_index

added theorem Polynomial.sum_def

added theorem Polynomial.sum_eq_of_subset

added theorem Polynomial.sum_monomial_eq

added theorem Polynomial.sum_monomial_index

added theorem Polynomial.sum_smul_index

added theorem Polynomial.sum_zero_index

added def Polynomial.support

added theorem Polynomial.support_C_mul_X'

added theorem Polynomial.support_C_mul_X

added theorem Polynomial.support_C_mul_X_pow'

added theorem Polynomial.support_C_mul_X_pow

added theorem Polynomial.support_X

added theorem Polynomial.support_X_empty

added theorem Polynomial.support_X_pow

added theorem Polynomial.support_add

added theorem Polynomial.support_binomial'

added theorem Polynomial.support_eq_empty

added theorem Polynomial.support_erase

added theorem Polynomial.support_monomial'

added theorem Polynomial.support_monomial

added theorem Polynomial.support_neg

added theorem Polynomial.support_ofFinsupp

added theorem Polynomial.support_trinomial'

added theorem Polynomial.support_update

added theorem Polynomial.support_update_ne_zero

added theorem Polynomial.support_update_zero

added theorem Polynomial.support_zero

added def Polynomial.toFinsuppIso

added theorem Polynomial.toFinsupp_C

added theorem Polynomial.toFinsupp_C_mul_X

added theorem Polynomial.toFinsupp_C_mul_X_pow

added theorem Polynomial.toFinsupp_X

added theorem Polynomial.toFinsupp_X_pow

added theorem Polynomial.toFinsupp_add

added theorem Polynomial.toFinsupp_apply

added theorem Polynomial.toFinsupp_eq_one

added theorem Polynomial.toFinsupp_eq_zero

added theorem Polynomial.toFinsupp_erase

added theorem Polynomial.toFinsupp_inj

added theorem Polynomial.toFinsupp_injective

added theorem Polynomial.toFinsupp_monomial

added theorem Polynomial.toFinsupp_mul

added theorem Polynomial.toFinsupp_neg

added theorem Polynomial.toFinsupp_one

added theorem Polynomial.toFinsupp_pow

added theorem Polynomial.toFinsupp_smul

added theorem Polynomial.toFinsupp_sub

added theorem Polynomial.toFinsupp_sum

added theorem Polynomial.toFinsupp_zero

added def Polynomial.update

added theorem Polynomial.update_zero_eq_erase

added structure Polynomial