Commit 2023-03-08 11:06 d46c392e

View on Github →

feat: port Data.Polynomial.Degree.Definitions (#2631)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.C_mul_X_pow_eq_self

added theorem Polynomial.Monic.coeff_natDegree

added theorem Polynomial.Monic.def

added theorem Polynomial.Monic.degree_mul

added theorem Polynomial.Monic.eq_X_add_C

added theorem Polynomial.Monic.leadingCoeff

added theorem Polynomial.Monic.ne_zero

added theorem Polynomial.Monic.ne_zero_of_ne

added theorem Polynomial.Monic.ne_zero_of_polynomial_ne

added def Polynomial.Monic

added theorem Polynomial.X_add_C_ne_one

added theorem Polynomial.X_add_C_ne_zero

added theorem Polynomial.X_pow_add_C_ne_one

added theorem Polynomial.X_pow_add_C_ne_zero

added theorem Polynomial.X_pow_sub_C_ne_zero

added theorem Polynomial.X_sub_C_ne_zero

added theorem Polynomial.as_sum_range'

added theorem Polynomial.as_sum_range

added theorem Polynomial.as_sum_range_C_mul_X_pow

added theorem Polynomial.as_sum_support

added theorem Polynomial.as_sum_support_C_mul_X_pow

added theorem Polynomial.card_supp_le_succ_natDegree

added theorem Polynomial.card_support_C_mul_X_pow_le_one

added theorem Polynomial.coeff_eq_zero_of_degree_lt

added theorem Polynomial.coeff_eq_zero_of_natDegree_lt

added theorem Polynomial.coeff_mul_X_sub_C

added theorem Polynomial.coeff_mul_degree_add_degree

added theorem Polynomial.coeff_natDegree

added theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt

added theorem Polynomial.coeff_natDegree_succ_eq_zero

added theorem Polynomial.coeff_ne_zero_of_eq_degree

added theorem Polynomial.coeff_pow_mul_natDegree

added def Polynomial.degree

added def Polynomial.degreeMonoidHom

added theorem Polynomial.degree_C

added theorem Polynomial.degree_C_le

added theorem Polynomial.degree_C_lt

added theorem Polynomial.degree_C_lt_degree_C_mul_X

added theorem Polynomial.degree_C_mul_X

added theorem Polynomial.degree_C_mul_X_le

added theorem Polynomial.degree_C_mul_X_pow

added theorem Polynomial.degree_C_mul_X_pow_le

added theorem Polynomial.degree_X

added theorem Polynomial.degree_X_add_C

added theorem Polynomial.degree_X_le

added theorem Polynomial.degree_X_pow

added theorem Polynomial.degree_X_pow_add_C

added theorem Polynomial.degree_X_pow_le

added theorem Polynomial.degree_X_pow_sub_C

added theorem Polynomial.degree_X_sub_C

added theorem Polynomial.degree_X_sub_C_le

added theorem Polynomial.degree_add_C

added theorem Polynomial.degree_add_eq_left_of_degree_lt

added theorem Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero

added theorem Polynomial.degree_add_eq_right_of_degree_lt

added theorem Polynomial.degree_add_le

added theorem Polynomial.degree_add_le_of_degree_le

added theorem Polynomial.degree_cubic

added theorem Polynomial.degree_cubic_le

added theorem Polynomial.degree_cubic_lt

added theorem Polynomial.degree_eq_bot

added theorem Polynomial.degree_eq_iff_natDegree_eq

added theorem Polynomial.degree_eq_iff_natDegree_eq_of_pos

added theorem Polynomial.degree_eq_natDegree

added theorem Polynomial.degree_eq_of_le_of_coeff_ne_zero

added theorem Polynomial.degree_erase_le

added theorem Polynomial.degree_erase_lt

added theorem Polynomial.degree_le_degree

added theorem Polynomial.degree_le_iff_coeff_zero

added theorem Polynomial.degree_le_natDegree

added theorem Polynomial.degree_le_zero_iff

added theorem Polynomial.degree_linear

added theorem Polynomial.degree_linear_le

added theorem Polynomial.degree_linear_lt

added theorem Polynomial.degree_linear_lt_degree_C_mul_X_sq

added theorem Polynomial.degree_lt_degree

added theorem Polynomial.degree_lt_degree_mul_x

added theorem Polynomial.degree_lt_iff_coeff_zero

added theorem Polynomial.degree_lt_wf

added theorem Polynomial.degree_mono

added theorem Polynomial.degree_monomial

added theorem Polynomial.degree_monomial_le

added theorem Polynomial.degree_mul'

added theorem Polynomial.degree_mul

added theorem Polynomial.degree_mul_X

added theorem Polynomial.degree_mul_X_pow

added theorem Polynomial.degree_mul_le

added theorem Polynomial.degree_ne_of_natDegree_ne

added theorem Polynomial.degree_neg

added theorem Polynomial.degree_of_subsingleton

added theorem Polynomial.degree_one

added theorem Polynomial.degree_one_le

added theorem Polynomial.degree_pow'

added theorem Polynomial.degree_pow

added theorem Polynomial.degree_pow_le

added theorem Polynomial.degree_quadratic

added theorem Polynomial.degree_quadratic_le

added theorem Polynomial.degree_quadratic_lt

added theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb

added theorem Polynomial.degree_smul_le

added theorem Polynomial.degree_sub_eq_left_of_degree_lt

added theorem Polynomial.degree_sub_eq_right_of_degree_lt

added theorem Polynomial.degree_sub_le

added theorem Polynomial.degree_sub_lt

added theorem Polynomial.degree_sum_fin_lt

added theorem Polynomial.degree_sum_le

added theorem Polynomial.degree_update_le

added theorem Polynomial.degree_zero

added theorem Polynomial.eq_C_of_degree_eq_zero

added theorem Polynomial.eq_C_of_degree_le_zero

added theorem Polynomial.eq_C_of_natDegree_eq_zero

added theorem Polynomial.eq_C_of_natDegree_le_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.eq_X_add_C_of_natDegree_le_one

added theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one

added theorem Polynomial.ext_iff_degree_le

added theorem Polynomial.ext_iff_natDegree_le

added theorem Polynomial.ite_le_natDegree_coeff

added theorem Polynomial.le_degree_of_mem_supp

added theorem Polynomial.le_degree_of_ne_zero

added theorem Polynomial.le_natDegree_of_coe_le_degree

added theorem Polynomial.le_natDegree_of_mem_supp

added theorem Polynomial.le_natDegree_of_ne_zero

added def Polynomial.leadingCoeff

added def Polynomial.leadingCoeffHom

added theorem Polynomial.leadingCoeffHom_apply

added theorem Polynomial.leadingCoeff_C

added theorem Polynomial.leadingCoeff_C_mul_X

added theorem Polynomial.leadingCoeff_C_mul_X_pow

added theorem Polynomial.leadingCoeff_X

added theorem Polynomial.leadingCoeff_X_add_C

added theorem Polynomial.leadingCoeff_X_pow

added theorem Polynomial.leadingCoeff_X_pow_add_C

added theorem Polynomial.leadingCoeff_X_pow_add_one

added theorem Polynomial.leadingCoeff_X_pow_sub_C

added theorem Polynomial.leadingCoeff_X_pow_sub_one

added theorem Polynomial.leadingCoeff_X_sub_C

added theorem Polynomial.leadingCoeff_add_of_degree_eq

added theorem Polynomial.leadingCoeff_add_of_degree_lt

added theorem Polynomial.leadingCoeff_cubic

added theorem Polynomial.leadingCoeff_eq_zero

added theorem Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot

added theorem Polynomial.leadingCoeff_linear

added theorem Polynomial.leadingCoeff_monic_mul

added theorem Polynomial.leadingCoeff_monomial

added theorem Polynomial.leadingCoeff_mul'

added theorem Polynomial.leadingCoeff_mul

added theorem Polynomial.leadingCoeff_mul_X

added theorem Polynomial.leadingCoeff_mul_X_pow

added theorem Polynomial.leadingCoeff_mul_monic

added theorem Polynomial.leadingCoeff_ne_zero

added theorem Polynomial.leadingCoeff_neg

added theorem Polynomial.leadingCoeff_one

added theorem Polynomial.leadingCoeff_pow'

added theorem Polynomial.leadingCoeff_pow

added theorem Polynomial.leadingCoeff_pow_X_add_C

added theorem Polynomial.leadingCoeff_quadratic

added theorem Polynomial.leadingCoeff_zero

added theorem Polynomial.mem_support_C_mul_X_pow

added theorem Polynomial.monic_X

added theorem Polynomial.monic_X_pow

added theorem Polynomial.monic_of_degree_le_of_coeff_eq_one

added theorem Polynomial.monic_of_natDegree_le_of_coeff_eq_one

added theorem Polynomial.monic_of_subsingleton

added theorem Polynomial.monic_one

added theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self

added def Polynomial.natDegree

added theorem Polynomial.natDegree_C

added theorem Polynomial.natDegree_C_mul_X

added theorem Polynomial.natDegree_C_mul_X_pow

added theorem Polynomial.natDegree_C_mul_X_pow_le

added theorem Polynomial.natDegree_X

added theorem Polynomial.natDegree_X_add_C

added theorem Polynomial.natDegree_X_le

added theorem Polynomial.natDegree_X_pow

added theorem Polynomial.natDegree_X_pow_add_C

added theorem Polynomial.natDegree_X_pow_le

added theorem Polynomial.natDegree_X_pow_sub_C

added theorem Polynomial.natDegree_X_sub_C

added theorem Polynomial.natDegree_X_sub_C_le

added theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt

added theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt

added theorem Polynomial.natDegree_add_le

added theorem Polynomial.natDegree_add_le_of_degree_le

added theorem Polynomial.natDegree_cubic

added theorem Polynomial.natDegree_cubic_le

added theorem Polynomial.natDegree_eq_of_degree_eq

added theorem Polynomial.natDegree_eq_of_degree_eq_some

added theorem Polynomial.natDegree_eq_of_le_of_coeff_ne_zero

added theorem Polynomial.natDegree_eq_support_max'

added theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero

added theorem Polynomial.natDegree_int_cast

added theorem Polynomial.natDegree_le_iff_degree_le

added theorem Polynomial.natDegree_le_natDegree

added theorem Polynomial.natDegree_linear

added theorem Polynomial.natDegree_linear_le

added theorem Polynomial.natDegree_lt_iff_degree_lt

added theorem Polynomial.natDegree_lt_natDegree

added theorem Polynomial.natDegree_lt_natDegree_iff

added theorem Polynomial.natDegree_mem_support_of_nonzero

added theorem Polynomial.natDegree_monomial

added theorem Polynomial.natDegree_monomial_eq

added theorem Polynomial.natDegree_monomial_le

added theorem Polynomial.natDegree_mul'

added theorem Polynomial.natDegree_mul_le

added theorem Polynomial.natDegree_nat_cast

added theorem Polynomial.natDegree_neg

added theorem Polynomial.natDegree_of_subsingleton

added theorem Polynomial.natDegree_one

added theorem Polynomial.natDegree_pos_iff_degree_pos

added theorem Polynomial.natDegree_pow'

added theorem Polynomial.natDegree_pow_le

added theorem Polynomial.natDegree_quadratic

added theorem Polynomial.natDegree_quadratic_le

added theorem Polynomial.natDegree_smul_le

added theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt

added theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt

added theorem Polynomial.natDegree_sub_le

added theorem Polynomial.natDegree_zero

added theorem Polynomial.ne_zero_of_coe_le_degree

added theorem Polynomial.ne_zero_of_degree_ge_degree

added theorem Polynomial.ne_zero_of_degree_gt

added theorem Polynomial.ne_zero_of_natDegree_gt

added def Polynomial.nextCoeff

added theorem Polynomial.nextCoeff_C_eq_zero

added theorem Polynomial.nextCoeff_X_add_C

added theorem Polynomial.nextCoeff_X_sub_C

added theorem Polynomial.nextCoeff_of_pos_natDegree

added theorem Polynomial.nonempty_support_iff

added theorem Polynomial.not_isUnit_X

added theorem Polynomial.sum_fin

added theorem Polynomial.sum_over_range'

added theorem Polynomial.sum_over_range

added theorem Polynomial.supp_subset_range

added theorem Polynomial.supp_subset_range_natDegree_succ

added theorem Polynomial.zero_le_degree_iff

added theorem Polynomial.zero_nmem_multiset_map_X_add_C

added theorem Polynomial.zero_nmem_multiset_map_X_sub_C