Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-08 12:43 85d9f218

View on Github →

feat(*): localized R[X] notation for polynomial R (#11895) I did not change polynomial (complex_term_here taking args) in many places because I thought it would be more confusing. Also, in some files that prove things about polynomials incidentally, I also did not include the notation and change the files.

Estimated changes

modified def cubic.equiv
modified def cubic.to_poly
modified theorem polynomial.eval_smul'
modified theorem polynomial.smul_X
modified theorem polynomial.smul_eval
modified theorem polynomial.smul_eval_smul
modified theorem polynomial.adjoin_X
modified def polynomial.aeval
modified theorem polynomial.aeval_X
modified theorem polynomial.aeval_X_left
modified theorem polynomial.aeval_X_pow
modified theorem polynomial.aeval_def
modified theorem polynomial.aeval_fn_apply
modified theorem polynomial.aeval_nat_cast
modified theorem polynomial.aeval_one
modified theorem polynomial.aeval_sum
modified theorem polynomial.aeval_zero
modified theorem polynomial.alg_hom_ext
modified theorem polynomial.eval_mul_X_sub_C
modified theorem polynomial.eval_unique
modified def polynomial.C
modified theorem polynomial.C_eq_nat_cast
modified def polynomial.X
modified theorem polynomial.X_ne_zero
modified theorem polynomial.add_hom_ext'
modified theorem polynomial.add_hom_ext
modified theorem polynomial.add_to_finsupp
modified def polynomial.coeff
modified theorem polynomial.coeff_X
modified theorem polynomial.coeff_X_one
modified theorem polynomial.coeff_X_zero
modified theorem polynomial.coeff_erase
modified theorem polynomial.coeff_neg
modified theorem polynomial.coeff_one_zero
modified theorem polynomial.coeff_sub
modified theorem polynomial.coeff_update
modified theorem polynomial.coeff_update_ne
modified theorem polynomial.coeff_zero
modified theorem polynomial.commute_X
modified theorem polynomial.commute_X_pow
modified theorem polynomial.erase_ne
modified theorem polynomial.erase_same
modified theorem polynomial.erase_zero
modified theorem polynomial.ext
modified theorem polynomial.ext_iff
modified theorem polynomial.lhom_ext'
modified def polynomial.monomial
modified theorem polynomial.mul_to_finsupp
modified theorem polynomial.nat_cast_mul
modified theorem polynomial.neg_to_finsupp
modified theorem polynomial.one_to_finsupp
modified def polynomial.sum
modified theorem polynomial.sum_add'
modified theorem polynomial.sum_add
modified theorem polynomial.sum_add_index
modified theorem polynomial.sum_def
modified theorem polynomial.sum_eq_of_subset
modified theorem polynomial.sum_smul_index
modified def polynomial.support
modified theorem polynomial.support_X
modified theorem polynomial.support_X_empty
modified theorem polynomial.support_X_pow
modified theorem polynomial.support_erase
modified theorem polynomial.support_neg
modified theorem polynomial.support_update
modified theorem polynomial.support_zero
modified def polynomial.update
modified theorem polynomial.zero_to_finsupp
modified theorem polynomial.C_mul'
modified theorem polynomial.coeff_C_mul
modified theorem polynomial.coeff_C_mul_X
modified theorem polynomial.coeff_X_mul
modified theorem polynomial.coeff_X_mul_zero
modified theorem polynomial.coeff_X_pow_mul'
modified theorem polynomial.coeff_X_pow_mul
modified theorem polynomial.coeff_add
modified theorem polynomial.coeff_bit0_mul
modified theorem polynomial.coeff_bit1_mul
modified theorem polynomial.coeff_mul
modified theorem polynomial.coeff_mul_C
modified theorem polynomial.coeff_mul_X
modified theorem polynomial.coeff_mul_X_pow'
modified theorem polynomial.coeff_mul_X_pow
modified theorem polynomial.coeff_mul_X_zero
modified theorem polynomial.coeff_one
modified theorem polynomial.coeff_smul
modified theorem polynomial.coeff_sum
modified theorem polynomial.finset_sum_coeff
modified def polynomial.lcoeff
modified theorem polynomial.lcoeff_apply
modified theorem polynomial.mul_coeff_zero
modified theorem polynomial.support_smul
modified theorem polynomial.as_sum_range'
modified theorem polynomial.as_sum_range
modified theorem polynomial.as_sum_support
modified def polynomial.degree
modified theorem polynomial.degree_X
modified theorem polynomial.degree_X_le
modified theorem polynomial.degree_X_pow
modified theorem polynomial.degree_X_pow_le
modified theorem polynomial.degree_add_le
modified theorem polynomial.degree_erase_le
modified theorem polynomial.degree_lt_wf
modified theorem polynomial.degree_mono
modified theorem polynomial.degree_mul_le
modified theorem polynomial.degree_neg
modified theorem polynomial.degree_one
modified theorem polynomial.degree_one_le
modified theorem polynomial.degree_pow
modified theorem polynomial.degree_pow_le
modified theorem polynomial.degree_smul_le
modified theorem polynomial.degree_sub_le
modified theorem polynomial.degree_sum_le
modified theorem polynomial.degree_update_le
modified theorem polynomial.degree_zero
modified theorem polynomial.leading_coeff_X
modified theorem polynomial.monic.ne_zero
modified def polynomial.monic
modified theorem polynomial.monic_X
modified theorem polynomial.monic_X_pow
modified theorem polynomial.monic_one
modified def polynomial.nat_degree
modified theorem polynomial.nat_degree_X
modified theorem polynomial.nat_degree_X_le
modified theorem polynomial.nat_degree_X_pow
modified theorem polynomial.nat_degree_neg
modified theorem polynomial.nat_degree_one
modified theorem polynomial.nat_degree_zero
modified def polynomial.next_coeff
modified theorem polynomial.not_is_unit_X
modified theorem polynomial.sum_over_range'
modified theorem polynomial.sum_over_range
modified theorem polynomial.coe_lt_degree
modified theorem denoms_clearable.add
modified def denoms_clearable
modified theorem one_le_pow_mul_abs_eval_div
modified theorem polynomial.coeff_derivative
modified def polynomial.derivative
modified theorem polynomial.derivative_C_mul
modified theorem polynomial.derivative_X
modified theorem polynomial.derivative_add
modified theorem polynomial.derivative_apply
modified theorem polynomial.derivative_bit0
modified theorem polynomial.derivative_bit1
modified theorem polynomial.derivative_comp
modified theorem polynomial.derivative_eval
modified theorem polynomial.derivative_map
modified theorem polynomial.derivative_mul
modified theorem polynomial.derivative_neg
modified theorem polynomial.derivative_one
modified theorem polynomial.derivative_pow
modified theorem polynomial.derivative_prod
modified theorem polynomial.derivative_smul
modified theorem polynomial.derivative_sub
modified theorem polynomial.derivative_sum
modified theorem polynomial.derivative_zero
modified theorem polynomial.X_dvd_iff
modified theorem polynomial.div_by_monic_one
modified theorem polynomial.map_dvd_map
modified theorem polynomial.mod_by_monic_X
modified theorem polynomial.mod_by_monic_one
modified def polynomial.erase_lead
modified theorem polynomial.erase_lead_X
modified theorem polynomial.erase_lead_X_pow
modified theorem polynomial.erase_lead_zero
modified theorem polynomial.bit0_comp
modified theorem polynomial.bit1_comp
modified theorem polynomial.cast_int_comp
modified def polynomial.comp
modified theorem polynomial.comp_assoc
modified theorem polynomial.comp_zero
modified theorem polynomial.degree_map_le
modified def polynomial.eval
modified theorem polynomial.eval_finset_sum
modified theorem polynomial.eval_int_cast
modified theorem polynomial.eval_list_prod
modified theorem polynomial.eval_nat_cast
modified theorem polynomial.eval_neg
modified theorem polynomial.eval_one
modified theorem polynomial.eval_one_map
modified theorem polynomial.eval_prod
modified theorem polynomial.eval_smul
modified theorem polynomial.eval_sub
modified theorem polynomial.eval_sum
modified theorem polynomial.eval_zero
modified theorem polynomial.eval_zero_map
modified def polynomial.eval₂
modified theorem polynomial.eval₂_nat_cast
modified theorem polynomial.eval₂_one
modified theorem polynomial.eval₂_smul
modified theorem polynomial.eval₂_sum
modified theorem polynomial.eval₂_zero
modified theorem polynomial.is_root.dvd
modified theorem polynomial.is_root.map
modified theorem polynomial.is_root.of_map
modified def polynomial.is_root
modified theorem polynomial.is_root_map_iff
modified def polynomial.leval
modified def polynomial.map
modified theorem polynomial.map_comp
modified def polynomial.map_equiv
modified theorem polynomial.map_list_prod
modified theorem polynomial.map_one
modified theorem polynomial.map_prod
modified theorem polynomial.map_ring_hom_id
modified theorem polynomial.map_sum
modified theorem polynomial.map_zero
modified theorem polynomial.mem_map_srange
modified theorem polynomial.mul_comp
modified theorem polynomial.nat_cast_comp
modified theorem polynomial.one_comp
modified theorem polynomial.pow_comp
modified theorem polynomial.prod_comp
modified theorem polynomial.zero_comp
modified theorem polynomial.coe_norm_unit
modified theorem polynomial.coeff_inv_units
modified theorem polynomial.degree_div_le
modified theorem polynomial.degree_map
modified def polynomial.div
modified theorem polynomial.eval_gcd_eq_zero
modified theorem polynomial.map_dvd_map'
modified def polynomial.mod
modified theorem polynomial.monic_map_iff
modified theorem polynomial.roots_C_mul
modified theorem polynomial.roots_normalize
modified theorem polynomial.hasse_deriv_X
modified theorem polynomial.hasse_deriv_mul
modified theorem polynomial.sum_C_mul_X_eq
modified theorem polynomial.sum_monomial_eq
modified def polynomial.div_X
modified theorem polynomial.div_X_mul_X_add
modified theorem polynomial.iterated_deriv_X
modified theorem polynomial.X_mem_lifts
modified theorem polynomial.X_pow_mem_lifts
modified theorem polynomial.erase_mem_lifts
modified def polynomial.lifts
modified def polynomial.lifts_ring
modified theorem polynomial.map_alg_eq_map
modified theorem polynomial.mem_lifts
modified theorem polynomial.smul_mem_lifts
modified theorem polynomial.mirror_X
modified theorem polynomial.mirror_neg
modified theorem polynomial.mirror_smul
modified theorem polynomial.mirror_zero
modified theorem polynomial.monic.as_sum
modified theorem polynomial.monic.is_regular
modified theorem polynomial.next_coeff_map
modified theorem polynomial.not_monic_zero
modified theorem polynomial.ring_hom_ext'
modified theorem polynomial.ring_hom_ext
modified theorem polynomial.coeff_reflect
modified theorem polynomial.coeff_reverse
modified theorem polynomial.reflect_C_mul
modified theorem polynomial.reflect_add
modified theorem polynomial.reflect_monomial
modified theorem polynomial.reflect_neg
modified theorem polynomial.reflect_sub
modified theorem polynomial.reflect_support
modified theorem polynomial.reflect_zero
modified theorem polynomial.reverse_mul
modified theorem polynomial.reverse_neg
modified theorem polynomial.reverse_zero
modified theorem polynomial.card_roots'
modified theorem polynomial.card_roots_sub_C
modified theorem polynomial.count_roots
modified theorem polynomial.degree_coe_units
modified theorem polynomial.exists_max_root
modified theorem polynomial.exists_min_root
modified theorem polynomial.funext
modified theorem polynomial.irreducible_X
modified theorem polynomial.is_unit_iff
modified theorem polynomial.mem_roots_sub_C
modified theorem polynomial.nat_degree_pow
modified theorem polynomial.prime_X
modified def polynomial.root_set
modified theorem polynomial.root_set_def
modified theorem polynomial.root_set_finite
modified theorem polynomial.roots_list_prod
modified theorem polynomial.roots_mul
modified theorem polynomial.roots_one
modified theorem polynomial.roots_prod
modified theorem polynomial.roots_zero
modified theorem polynomial.sum_taylor_eq
modified def polynomial.taylor
modified theorem polynomial.taylor_eval
modified theorem polynomial.taylor_eval_sub
modified theorem polynomial.taylor_mul
modified theorem polynomial.taylor_one
modified theorem polynomial.taylor_taylor
modified theorem polynomial.taylor_zero
modified theorem gal_X_is_solvable
modified theorem gal_X_pow_is_solvable
modified theorem gal_is_solvable_of_splits
modified theorem gal_is_solvable_tower
modified theorem gal_mul_is_solvable
modified theorem gal_one_is_solvable
modified theorem gal_prod_is_solvable
modified theorem gal_zero_is_solvable
modified theorem finite_field.expand_card
modified theorem is_alg_closed.exists_root
modified theorem minpoly.dvd
modified theorem minpoly.eq_of_irreducible
modified theorem minpoly.min
modified theorem minpoly.unique
modified def ratfunc.X
modified theorem ratfunc.algebra_map_apply
modified theorem ratfunc.algebra_map_ne_zero
modified def ratfunc.denom
modified theorem ratfunc.denom_algebra_map
modified theorem ratfunc.denom_div
modified theorem ratfunc.denom_div_dvd
modified theorem ratfunc.denom_dvd
modified theorem ratfunc.div_smul
modified theorem ratfunc.eval_algebra_map
modified theorem ratfunc.lift_alg_hom_apply
modified theorem ratfunc.lift_on'_div
modified theorem ratfunc.lift_on'_mk
modified theorem ratfunc.lift_on_div
modified theorem ratfunc.lift_on_mk
modified def ratfunc.lift_ring_hom
modified def ratfunc.map
modified def ratfunc.map_alg_hom
modified theorem ratfunc.map_denom_ne_zero
modified theorem ratfunc.map_injective
modified def ratfunc.map_ring_hom
modified theorem ratfunc.mk_coe_def
modified theorem ratfunc.mk_def_of_mem
modified theorem ratfunc.mk_def_of_ne
modified theorem ratfunc.mk_eq_div'
modified theorem ratfunc.mk_eq_div
modified theorem ratfunc.mk_eq_mk
modified theorem ratfunc.mk_one'
modified theorem ratfunc.mk_one
modified theorem ratfunc.mk_smul
modified theorem ratfunc.mk_zero
modified def ratfunc.num
modified theorem ratfunc.num_algebra_map
modified def ratfunc.num_denom
modified theorem ratfunc.num_denom_div
modified theorem ratfunc.num_div
modified theorem ratfunc.num_div_dvd
modified theorem ratfunc.num_dvd
modified theorem irreducible.separable
modified theorem polynomial.coe_expand
modified theorem polynomial.coeff_contract
modified theorem polynomial.coeff_expand
modified theorem polynomial.coeff_expand_mul
modified theorem polynomial.contract_expand
modified theorem polynomial.expand_char
modified theorem polynomial.expand_contract
modified theorem polynomial.expand_eq_C
modified theorem polynomial.expand_eq_sum
modified theorem polynomial.expand_eq_zero
modified theorem polynomial.expand_eval
modified theorem polynomial.expand_expand
modified theorem polynomial.expand_inj
modified theorem polynomial.expand_mul
modified theorem polynomial.expand_one
modified theorem polynomial.expand_pow
modified theorem polynomial.expand_zero
modified theorem polynomial.map_expand
modified theorem polynomial.monic.expand
modified theorem polynomial.nodup_roots
modified theorem polynomial.separable.map
modified theorem polynomial.separable.mul
modified theorem polynomial.separable.of_dvd
modified theorem polynomial.separable.of_pow
modified def polynomial.separable
modified theorem polynomial.separable_X
modified theorem polynomial.separable_def'
modified theorem polynomial.separable_def
modified theorem polynomial.separable_map
modified theorem polynomial.separable_one
modified theorem polynomial.separable_or
modified theorem polynomial.separable_prod'
modified theorem polynomial.separable_prod
modified def polynomial.factor
modified theorem polynomial.roots_map
modified def polynomial.splits
modified theorem polynomial.splits_map_iff
modified theorem polynomial.splits_mul
modified theorem polynomial.splits_mul_iff
modified theorem polynomial.splits_pow
modified theorem polynomial.splits_prod
modified theorem polynomial.splits_prod_iff
modified theorem polynomial.splits_zero
modified def linear_map.charpoly
modified def lagrange.basis
modified theorem lagrange.eq_interpolate
modified theorem lagrange.eq_of_eval_eq
modified def lagrange.interpolate
modified def charmatrix
modified def matrix.charpoly
modified theorem matrix.eval_det
modified theorem matrix.mat_poly_equiv_eval
modified def polynomial.bernoulli
modified theorem adjoin_root.aeval_eq
modified def adjoin_root.equiv
modified theorem adjoin_root.eval₂_root
modified theorem adjoin_root.is_root_root
modified theorem adjoin_root.lift_hom_mk
modified theorem adjoin_root.lift_mk
modified def adjoin_root.mk
modified theorem adjoin_root.mk_eq_mk
modified def adjoin_root
modified theorem ideal.quotient_mk_maps_eq
modified theorem is_integral_trans_aux
modified def normalize_scale_roots
added theorem power_series.coe_neg
added theorem power_series.coe_sub
modified def ideal.degree_le
modified theorem ideal.mem_map_C_iff
modified def ideal.of_polynomial
modified theorem polynomial.coeff_mem_frange
modified theorem polynomial.coeff_of_subring
modified def polynomial.degree_le
modified def polynomial.degree_lt
modified def polynomial.frange
modified theorem polynomial.frange_one
modified theorem polynomial.frange_zero
modified theorem polynomial.map_restriction
modified theorem polynomial.mem_degree_le
modified theorem polynomial.mem_degree_lt
modified theorem polynomial.mem_frange_iff
modified def polynomial.of_subring
modified theorem polynomial.restriction_one
modified theorem polynomial.restriction_zero
modified def polynomial.to_subring
modified theorem polynomial.to_subring_one
modified theorem polynomial.to_subring_zero
modified def bernstein_polynomial
modified theorem polynomial.C_content_dvd
modified def polynomial.content
modified theorem polynomial.content_C_mul
modified theorem polynomial.content_X
modified theorem polynomial.content_X_mul
modified theorem polynomial.content_X_pow
modified theorem polynomial.content_mul
modified theorem polynomial.content_mul_aux
modified theorem polynomial.content_one
modified theorem polynomial.content_zero
modified theorem polynomial.is_primitive.mul
modified theorem polynomial.is_primitive_one
modified def polynomial.prim_part
modified theorem polynomial.prim_part_dvd
modified theorem polynomial.prim_part_mul
modified theorem polynomial.prim_part_zero
modified def polynomial.cyclotomic
modified structure polynomial.is_eisenstein_at
modified theorem denom_dvd_of_is_root
modified theorem num_dvd_of_is_root
modified theorem coeff_scale_roots
modified theorem degree_scale_roots
modified theorem monic_scale_roots_iff
modified theorem nat_degree_scale_roots
modified theorem scale_roots_aeval_eq_zero
modified theorem scale_roots_eval₂_eq_zero
modified theorem scale_roots_ne_zero
modified theorem support_scale_roots_eq
modified theorem support_scale_roots_le
modified theorem is_scalar_tower.aeval_apply
modified theorem subalgebra.aeval_coe
modified theorem mat_poly_equiv_smul_one
modified theorem poly_equiv_tensor.left_inv
modified theorem poly_equiv_tensor.right_inv
modified def poly_equiv_tensor
modified theorem poly_equiv_tensor_apply
modified theorem mv_power_series.map_X
modified theorem polynomial.coe_injective
modified theorem polynomial.coe_one
modified theorem polynomial.coe_zero
modified def power_series.trunc