Commit 2023-03-09 12:44 0ee6690d

View on Github →

feat: port Data.Polynomial.Monic (#2745)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Monic.lean

added theorem Function.Injective.monic_map_iff

added theorem Polynomial.Monic.add_of_left

added theorem Polynomial.Monic.add_of_right

added theorem Polynomial.Monic.as_sum

added theorem Polynomial.Monic.degree_le_zero_iff_eq_one

added theorem Polynomial.Monic.degree_map

added theorem Polynomial.Monic.degree_mul_comm

added theorem Polynomial.Monic.eq_one_of_isUnit

added theorem Polynomial.Monic.eq_one_of_map_eq_one

added theorem Polynomial.Monic.isRegular

added theorem Polynomial.Monic.isUnit_iff

added theorem Polynomial.Monic.map

added theorem Polynomial.Monic.mul

added theorem Polynomial.Monic.mul_left_eq_zero_iff

added theorem Polynomial.Monic.mul_left_ne_zero

added theorem Polynomial.Monic.mul_natDegree_lt_iff

added theorem Polynomial.Monic.mul_right_eq_zero_iff

added theorem Polynomial.Monic.mul_right_ne_zero

added theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one

added theorem Polynomial.Monic.natDegree_map

added theorem Polynomial.Monic.natDegree_mul

added theorem Polynomial.Monic.natDegree_mul_comm

added theorem Polynomial.Monic.natDegree_pow

added theorem Polynomial.Monic.nextCoeff_mul

added theorem Polynomial.Monic.nextCoeff_multiset_prod

added theorem Polynomial.Monic.nextCoeff_prod

added theorem Polynomial.Monic.not_dvd_of_degree_lt

added theorem Polynomial.Monic.not_dvd_of_natDegree_lt

added theorem Polynomial.Monic.of_mul_monic_left

added theorem Polynomial.Monic.of_mul_monic_right

added theorem Polynomial.Monic.pow

added theorem Polynomial.Monic.sub_of_left

added theorem Polynomial.Monic.sub_of_right

added theorem Polynomial.degree_map_eq_of_injective

added theorem Polynomial.degree_smul_of_smul_regular

added theorem Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff

added theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff

added theorem Polynomial.leadingCoeff_map'

added theorem Polynomial.leadingCoeff_of_injective

added theorem Polynomial.leadingCoeff_smul_of_smul_regular

added theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one

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_pow_sub_C

added theorem Polynomial.monic_X_sub_C

added theorem Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one

added theorem Polynomial.monic_multiset_prod_of_monic

added theorem Polynomial.monic_of_degree_le

added theorem Polynomial.monic_of_injective

added theorem Polynomial.monic_of_isUnit_leadingCoeff_inv_smul

added theorem Polynomial.monic_prod_of_monic

added theorem Polynomial.monic_zero_iff_subsingleton'

added theorem Polynomial.monic_zero_iff_subsingleton

added theorem Polynomial.natDegree_map_eq_of_injective

added theorem Polynomial.natDegree_pow_X_add_c

added theorem Polynomial.natDegree_smul_of_smul_regular

added theorem Polynomial.ne_zero_of_ne_zero_of_monic

added theorem Polynomial.nextCoeff_map

added theorem Polynomial.not_isUnit_X_pow_sub_one

added theorem Polynomial.not_monic_zero

added theorem Polynomial.not_monic_zero_iff