Commit 2024-11-15 09:38 12f31632

View on Github →

chore(Algebra/Polynomial/Degree): split Definitions.lean (#19038) This file was very big and contained many more things than just the definitions of Polynomial.degree et al. This PR splits off the following files:

Degree/Operations.lean: lemmas to compute the degree for various ring operations (this is probably the file to import if you're missing something after merging this PR)
Degree/Domain.lean: Polynomial.instIsDomain instance and its consequences
Degree/Monomial.lean: lemmas to compute the degree for monomials
Degree/SmallDegree.lean: lemmas where the degree is a specific small number such as 2 or 3
Degree/Support.lean: lemmas about writing polynomials as sum over the support
Degree/Units.lean: lemmas about the degree of units

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/CancelLeads.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

deleted theorem Polynomial.C_mul_X_pow_eq_self

deleted theorem Polynomial.Monic.C_dvd_iff_isUnit

deleted theorem Polynomial.Monic.degree_mul

deleted theorem Polynomial.Monic.degree_pos

deleted theorem Polynomial.Monic.degree_pos_of_not_isUnit

deleted theorem Polynomial.Monic.eq_X_add_C

deleted theorem Polynomial.Monic.natDegree_eq_zero

deleted theorem Polynomial.Monic.natDegree_pos

deleted theorem Polynomial.Monic.natDegree_pos_of_not_isUnit

deleted theorem Polynomial.X_add_C_ne_one

deleted theorem Polynomial.X_add_C_ne_zero

deleted theorem Polynomial.X_pow_add_C_ne_one

deleted theorem Polynomial.X_pow_add_C_ne_zero

deleted theorem Polynomial.X_pow_sub_C_ne_zero

deleted theorem Polynomial.X_sub_C_ne_zero

deleted theorem Polynomial.as_sum_range'

deleted theorem Polynomial.as_sum_range

deleted theorem Polynomial.as_sum_range_C_mul_X_pow

deleted theorem Polynomial.as_sum_support

deleted theorem Polynomial.as_sum_support_C_mul_X_pow

deleted theorem Polynomial.card_supp_le_succ_natDegree

deleted theorem Polynomial.card_support_C_mul_X_pow_le_one

deleted theorem Polynomial.coeff_coe_units_zero_ne_zero

deleted theorem Polynomial.coeff_eq_zero_of_degree_lt

deleted theorem Polynomial.coeff_eq_zero_of_natDegree_lt

deleted theorem Polynomial.coeff_mul_X_sub_C

deleted theorem Polynomial.coeff_mul_add_eq_of_natDegree_le

deleted theorem Polynomial.coeff_mul_degree_add_degree

deleted theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt

deleted theorem Polynomial.coeff_natDegree_succ_eq_zero

deleted theorem Polynomial.coeff_pow_mul_natDegree

deleted def Polynomial.degreeMonoidHom

deleted theorem Polynomial.degree_C_lt_degree_C_mul_X

deleted theorem Polynomial.degree_X_add_C

deleted theorem Polynomial.degree_X_pow_add_C

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_eq_left_of_degree_lt

deleted theorem Polynomial.degree_add_eq_of_leadingCoeff_add_ne_zero

deleted theorem Polynomial.degree_add_eq_right_of_degree_lt

deleted theorem Polynomial.degree_coe_units

deleted theorem Polynomial.degree_cubic

deleted theorem Polynomial.degree_cubic_le

deleted theorem Polynomial.degree_cubic_lt

deleted theorem Polynomial.degree_eq_of_le_of_coeff_ne_zero

deleted theorem Polynomial.degree_eq_zero_of_isUnit

deleted theorem Polynomial.degree_le_mul_left

deleted theorem Polynomial.degree_le_of_dvd

deleted theorem Polynomial.degree_le_zero_iff

deleted theorem Polynomial.degree_linear

deleted theorem Polynomial.degree_linear_le

deleted theorem Polynomial.degree_linear_lt

deleted theorem Polynomial.degree_linear_lt_degree_C_mul_X_sq

deleted theorem Polynomial.degree_lt_degree

deleted theorem Polynomial.degree_lt_degree_mul_X

deleted theorem Polynomial.degree_lt_wf

deleted theorem Polynomial.degree_mul'

deleted theorem Polynomial.degree_mul

deleted theorem Polynomial.degree_mul_X

deleted theorem Polynomial.degree_mul_X_pow

deleted theorem Polynomial.degree_of_subsingleton

deleted theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic

deleted theorem Polynomial.degree_pow'

deleted theorem Polynomial.degree_pow

deleted theorem Polynomial.degree_quadratic

deleted theorem Polynomial.degree_quadratic_le

deleted theorem Polynomial.degree_quadratic_lt

deleted theorem Polynomial.degree_quadratic_lt_degree_C_mul_X_cb

deleted theorem Polynomial.degree_smul_le

deleted theorem Polynomial.degree_sub_C

deleted theorem Polynomial.degree_sub_eq_left_of_degree_lt

deleted theorem Polynomial.degree_sub_eq_right_of_degree_lt

deleted theorem Polynomial.degree_sum_fin_lt

deleted theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_zero

deleted theorem Polynomial.eq_C_of_degree_eq_zero

deleted theorem Polynomial.eq_C_of_degree_le_zero

deleted theorem Polynomial.eq_C_of_natDegree_eq_zero

deleted theorem Polynomial.eq_C_of_natDegree_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_X_add_C_of_natDegree_le_one

deleted theorem Polynomial.eq_one_of_monic_natDegree_zero

deleted theorem Polynomial.eq_zero_of_dvd_of_degree_lt

deleted theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt

deleted theorem Polynomial.exists_eq_X_add_C_of_natDegree_le_one

deleted theorem Polynomial.ext_iff_degree_le

deleted theorem Polynomial.ext_iff_natDegree_le

deleted theorem Polynomial.isUnit_iff

deleted theorem Polynomial.ite_le_natDegree_coeff

deleted theorem Polynomial.le_degree_of_mem_supp

deleted theorem Polynomial.le_natDegree_of_coe_le_degree

deleted theorem Polynomial.le_natDegree_of_mem_supp

deleted theorem Polynomial.le_natDegree_of_ne_zero

deleted def Polynomial.leadingCoeffHom

deleted theorem Polynomial.leadingCoeffHom_apply

deleted theorem Polynomial.leadingCoeff_X_add_C

deleted theorem Polynomial.leadingCoeff_X_pow_add_C

deleted theorem Polynomial.leadingCoeff_X_pow_add_one

deleted theorem Polynomial.leadingCoeff_X_pow_sub_C

deleted theorem Polynomial.leadingCoeff_X_pow_sub_one

deleted theorem Polynomial.leadingCoeff_X_sub_C

deleted theorem Polynomial.leadingCoeff_add_of_degree_eq

deleted theorem Polynomial.leadingCoeff_add_of_degree_lt'

deleted theorem Polynomial.leadingCoeff_add_of_degree_lt

deleted theorem Polynomial.leadingCoeff_cubic

deleted theorem Polynomial.leadingCoeff_dvd_leadingCoeff

deleted theorem Polynomial.leadingCoeff_linear

deleted theorem Polynomial.leadingCoeff_monic_mul

deleted theorem Polynomial.leadingCoeff_mul'

deleted theorem Polynomial.leadingCoeff_mul

deleted theorem Polynomial.leadingCoeff_mul_X

deleted theorem Polynomial.leadingCoeff_mul_X_pow

deleted theorem Polynomial.leadingCoeff_mul_monic

deleted theorem Polynomial.leadingCoeff_pow'

deleted theorem Polynomial.leadingCoeff_pow

deleted theorem Polynomial.leadingCoeff_pow_X_add_C

deleted theorem Polynomial.leadingCoeff_quadratic

deleted theorem Polynomial.leadingCoeff_sub_of_degree_eq

deleted theorem Polynomial.leadingCoeff_sub_of_degree_lt'

deleted theorem Polynomial.leadingCoeff_sub_of_degree_lt

deleted theorem Polynomial.mem_support_C_mul_X_pow

deleted theorem Polynomial.monic_of_degree_le_of_coeff_eq_one

deleted theorem Polynomial.monic_of_natDegree_le_of_coeff_eq_one

deleted theorem Polynomial.monic_of_subsingleton

deleted theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self

deleted theorem Polynomial.natDegree_C_add

deleted theorem Polynomial.natDegree_X_add_C

deleted theorem Polynomial.natDegree_X_mul

deleted theorem Polynomial.natDegree_X_pow_add_C

deleted theorem Polynomial.natDegree_X_pow_le

deleted theorem Polynomial.natDegree_X_pow_mul

deleted theorem Polynomial.natDegree_X_pow_sub_C

deleted theorem Polynomial.natDegree_X_sub_C

deleted theorem Polynomial.natDegree_add_C

deleted theorem Polynomial.natDegree_add_eq_left_of_degree_lt

deleted theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt

deleted theorem Polynomial.natDegree_add_eq_right_of_degree_lt

deleted theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt

deleted theorem Polynomial.natDegree_coe_units

deleted theorem Polynomial.natDegree_cubic

deleted theorem Polynomial.natDegree_cubic_le

deleted theorem Polynomial.natDegree_eq_of_le_of_coeff_ne_zero

deleted theorem Polynomial.natDegree_eq_of_natDegree_add_eq_zero

deleted theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left

deleted theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right

deleted theorem Polynomial.natDegree_eq_support_max'

deleted theorem Polynomial.natDegree_eq_zero

deleted theorem Polynomial.natDegree_eq_zero_of_isUnit

deleted theorem Polynomial.natDegree_le_of_dvd

deleted theorem Polynomial.natDegree_le_pred

deleted theorem Polynomial.natDegree_linear

deleted theorem Polynomial.natDegree_linear_le

deleted theorem Polynomial.natDegree_lt_natDegree

deleted theorem Polynomial.natDegree_lt_natDegree_iff

deleted theorem Polynomial.natDegree_mem_support_of_nonzero

deleted theorem Polynomial.natDegree_mul'

deleted theorem Polynomial.natDegree_mul

deleted theorem Polynomial.natDegree_mul_X

deleted theorem Polynomial.natDegree_mul_X_pow

deleted theorem Polynomial.natDegree_of_subsingleton

deleted theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic

deleted theorem Polynomial.natDegree_pow'

deleted theorem Polynomial.natDegree_pow

deleted theorem Polynomial.natDegree_quadratic

deleted theorem Polynomial.natDegree_quadratic_le

deleted theorem Polynomial.natDegree_smul_le

deleted theorem Polynomial.natDegree_sub_C

deleted theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt

deleted theorem Polynomial.natDegree_sub_eq_of_prod_eq

deleted theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt

deleted theorem Polynomial.ne_zero_of_coe_le_degree

deleted theorem Polynomial.ne_zero_of_degree_ge_degree

deleted theorem Polynomial.ne_zero_of_degree_gt

deleted theorem Polynomial.ne_zero_of_natDegree_gt

deleted theorem Polynomial.nextCoeff_X_add_C

deleted theorem Polynomial.nextCoeff_X_sub_C

deleted theorem Polynomial.nonempty_support_iff

deleted theorem Polynomial.not_dvd_of_degree_lt

deleted theorem Polynomial.not_dvd_of_natDegree_lt

deleted theorem Polynomial.not_isUnit_X

deleted theorem Polynomial.not_isUnit_of_degree_pos

deleted theorem Polynomial.not_isUnit_of_natDegree_pos

deleted theorem Polynomial.sum_fin

deleted theorem Polynomial.sum_over_range'

deleted theorem Polynomial.sum_over_range

deleted theorem Polynomial.supDegree_eq_degree

deleted theorem Polynomial.supDegree_eq_natDegree

deleted theorem Polynomial.supp_subset_range

deleted theorem Polynomial.supp_subset_range_natDegree_succ

deleted theorem Polynomial.zero_le_degree_iff

deleted theorem Polynomial.zero_nmem_multiset_map_X_add_C

deleted theorem Polynomial.zero_nmem_multiset_map_X_sub_C

Created Mathlib/Algebra/Polynomial/Degree/Domain.lean

added theorem Polynomial.degree_le_of_dvd

added theorem Polynomial.eq_zero_of_dvd_of_degree_lt

added theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt

added theorem Polynomial.natDegree_le_of_dvd

added theorem Polynomial.natDegree_mul

added theorem Polynomial.natDegree_pow

added theorem Polynomial.natDegree_sub_eq_of_prod_eq

added theorem Polynomial.not_dvd_of_degree_lt

added theorem Polynomial.not_dvd_of_natDegree_lt

Created Mathlib/Algebra/Polynomial/Degree/Monomial.lean

added theorem Polynomial.C_mul_X_pow_eq_self

added theorem Polynomial.monomial_natDegree_leadingCoeff_eq_self

added theorem Polynomial.natDegree_le_pred

Created Mathlib/Algebra/Polynomial/Degree/Operations.lean

added theorem Polynomial.Monic.degree_mul

added theorem Polynomial.Monic.degree_pos

added theorem Polynomial.Monic.natDegree_eq_zero

added theorem Polynomial.Monic.natDegree_pos

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

added theorem Polynomial.coeff_mul_degree_add_degree

added theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt

added theorem Polynomial.coeff_natDegree_succ_eq_zero

added theorem Polynomial.coeff_pow_mul_natDegree

added def Polynomial.degreeMonoidHom

added theorem Polynomial.degree_C_lt_degree_C_mul_X

added theorem Polynomial.degree_X_add_C

added theorem Polynomial.degree_X_pow_add_C

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_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_eq_of_le_of_coeff_ne_zero

added theorem Polynomial.degree_le_mul_left

added theorem Polynomial.degree_le_zero_iff

added theorem Polynomial.degree_lt_degree

added theorem Polynomial.degree_lt_degree_mul_X

added theorem Polynomial.degree_lt_wf

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_of_subsingleton

added theorem Polynomial.degree_pow'

added theorem Polynomial.degree_pow

added theorem Polynomial.degree_smul_le

added theorem Polynomial.degree_sub_C

added theorem Polynomial.degree_sub_eq_left_of_degree_lt

added theorem Polynomial.degree_sub_eq_right_of_degree_lt

added theorem Polynomial.degree_sum_fin_lt

added theorem Polynomial.eq_C_coeff_zero_iff_natDegree_eq_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_one_of_monic_natDegree_zero

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_natDegree_of_ne_zero

added def Polynomial.leadingCoeffHom

added theorem Polynomial.leadingCoeffHom_apply

added theorem Polynomial.leadingCoeff_X_add_C

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_add_of_degree_lt

added theorem Polynomial.leadingCoeff_dvd_leadingCoeff

added theorem Polynomial.leadingCoeff_monic_mul

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_pow'

added theorem Polynomial.leadingCoeff_pow

added theorem Polynomial.leadingCoeff_pow_X_add_C

added theorem Polynomial.leadingCoeff_sub_of_degree_eq

added theorem Polynomial.leadingCoeff_sub_of_degree_lt'

added theorem Polynomial.leadingCoeff_sub_of_degree_lt

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

added theorem Polynomial.natDegree_X_add_C

added theorem Polynomial.natDegree_X_mul

added theorem Polynomial.natDegree_X_pow_add_C

added theorem Polynomial.natDegree_X_pow_le

added theorem Polynomial.natDegree_X_pow_mul

added theorem Polynomial.natDegree_X_pow_sub_C

added theorem Polynomial.natDegree_X_sub_C

added theorem Polynomial.natDegree_add_C

added theorem Polynomial.natDegree_add_eq_left_of_degree_lt

added theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt

added theorem Polynomial.natDegree_add_eq_right_of_degree_lt

added theorem Polynomial.natDegree_add_eq_right_of_natDegree_lt

added theorem Polynomial.natDegree_eq_of_le_of_coeff_ne_zero

added theorem Polynomial.natDegree_eq_of_natDegree_add_eq_zero

added theorem Polynomial.natDegree_eq_of_natDegree_add_lt_left

added theorem Polynomial.natDegree_eq_of_natDegree_add_lt_right

added theorem Polynomial.natDegree_eq_zero

added theorem Polynomial.natDegree_lt_natDegree

added theorem Polynomial.natDegree_lt_natDegree_iff

added theorem Polynomial.natDegree_mul'

added theorem Polynomial.natDegree_mul_X

added theorem Polynomial.natDegree_mul_X_pow

added theorem Polynomial.natDegree_of_subsingleton

added theorem Polynomial.natDegree_pow'

added theorem Polynomial.natDegree_smul_le

added theorem Polynomial.natDegree_sub_C

added theorem Polynomial.natDegree_sub_eq_left_of_natDegree_lt

added theorem Polynomial.natDegree_sub_eq_right_of_natDegree_lt

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 theorem Polynomial.nextCoeff_X_add_C

added theorem Polynomial.nextCoeff_X_sub_C

added theorem Polynomial.not_isUnit_X

added theorem Polynomial.supDegree_eq_degree

added theorem Polynomial.zero_nmem_multiset_map_X_add_C

added theorem Polynomial.zero_nmem_multiset_map_X_sub_C

Created Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean

added theorem Polynomial.Monic.eq_X_add_C

added theorem Polynomial.degree_cubic

added theorem Polynomial.degree_cubic_le

added theorem Polynomial.degree_cubic_lt

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_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.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.le_natDegree_of_coe_le_degree

added theorem Polynomial.leadingCoeff_cubic

added theorem Polynomial.leadingCoeff_linear

added theorem Polynomial.leadingCoeff_quadratic

added theorem Polynomial.natDegree_cubic

added theorem Polynomial.natDegree_cubic_le

added theorem Polynomial.natDegree_linear

added theorem Polynomial.natDegree_linear_le

added theorem Polynomial.natDegree_quadratic

added theorem Polynomial.natDegree_quadratic_le

added theorem Polynomial.ne_zero_of_coe_le_degree

added theorem Polynomial.zero_le_degree_iff

Created Mathlib/Algebra/Polynomial/Degree/Support.lean

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

added theorem Polynomial.le_natDegree_of_mem_supp

added theorem Polynomial.mem_support_C_mul_X_pow

added theorem Polynomial.natDegree_eq_support_max'

added theorem Polynomial.natDegree_mem_support_of_nonzero

added theorem Polynomial.nonempty_support_iff

added theorem Polynomial.sum_fin

added theorem Polynomial.sum_over_range'

added theorem Polynomial.sum_over_range

added theorem Polynomial.supDegree_eq_natDegree

added theorem Polynomial.supp_subset_range

added theorem Polynomial.supp_subset_range_natDegree_succ

Modified Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean

Created Mathlib/Algebra/Polynomial/Degree/Units.lean

added theorem Polynomial.Monic.C_dvd_iff_isUnit

added theorem Polynomial.Monic.degree_pos_of_not_isUnit

added theorem Polynomial.Monic.natDegree_pos_of_not_isUnit

added theorem Polynomial.coeff_coe_units_zero_ne_zero

added theorem Polynomial.degree_coe_units

added theorem Polynomial.degree_eq_zero_of_isUnit

added theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic

added theorem Polynomial.isUnit_iff

added theorem Polynomial.natDegree_coe_units

added theorem Polynomial.natDegree_eq_zero_of_isUnit

added theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic

added theorem Polynomial.not_isUnit_of_degree_pos

added theorem Polynomial.not_isUnit_of_natDegree_pos

Modified Mathlib/Algebra/Polynomial/EraseLead.lean

Modified Mathlib/Algebra/Polynomial/Eval.lean

Modified Mathlib/Algebra/Polynomial/Inductions.lean

Modified Mathlib/FieldTheory/RatFunc/Defs.lean

Modified Mathlib/RingTheory/Polynomial/Opposites.lean