Theoremsmonic_map_iff, add_of_left, add_of_right, as_sum, comp, comp_X_add_C, comp_X_sub_C, degree_le_zero_iff_eq_one, degree_map, degree_mul_comm, eq_one_of_isUnit, eq_one_of_map_eq_one, irreducible_iff_lt_natDegree_lt, irreducible_iff_natDegree, irreducible_iff_natDegree', isRegular, isUnit_iff, map, mul, mul_left_eq_zero_iff, mul_left_ne_zero, mul_natDegree_lt_iff, mul_right_eq_zero_iff, mul_right_ne_zero, natDegree_eq_zero_iff_eq_one, natDegree_map, natDegree_mul, natDegree_mul', natDegree_mul_comm, natDegree_pow, nextCoeff_mul, nextCoeff_multiset_prod, nextCoeff_pow, nextCoeff_prod, not_dvd_of_degree_lt, not_dvd_of_natDegree_lt, not_irreducible_iff_exists_add_mul_eq_coeff, of_mul_monic_left, of_mul_monic_right, pow, sub_of_left, sub_of_right, coeff_of_ge, degree, map_coe, mk_coe, monic, natDegree, degree_smul_of_smul_regular, eq_of_monic_of_associated, irreducible_of_monic, isUnit_leadingCoeff_mul_left_eq_zero_iff, isUnit_leadingCoeff_mul_right_eq_zero_iff, leadingCoeff_map', leadingCoeff_of_injective, leadingCoeff_smul_of_smul_regular, monic_C_mul_of_mul_leadingCoeff_eq_one, monic_X_add_C, monic_X_pow_add, monic_X_pow_add_C, monic_X_pow_sub, monic_X_pow_sub_C, monic_X_sub_C, monic_finprod_of_monic, monic_mul_C_of_leadingCoeff_mul_eq_one, monic_multiset_prod_of_monic, monic_of_injective, monic_of_isUnit_leadingCoeff_inv_smul, monic_prod_of_monic, monic_zero_iff_subsingleton, monic_zero_iff_subsingleton', natDegree_pow_X_add_C, natDegree_smul_of_smul_regular, not_isUnit_X_add_C, not_isUnit_X_pow_sub_one, not_monic_zero, not_monic_zero_iff | 77 |