Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-22 12:16 e4abcedc

View on Github →

chore(data/polynomial): rename type vars (#2483) Rename α to R etc; use ι for index types No other changes

Estimated changes

modified def polynomial.C
modified theorem polynomial.C_0
modified theorem polynomial.C_1
modified theorem polynomial.C_mul'
modified def polynomial.X
modified theorem polynomial.X_ne_zero
modified theorem polynomial.as_sum
modified theorem polynomial.card_nth_roots
modified theorem polynomial.card_roots'
modified theorem polynomial.card_roots_sub_C
modified theorem polynomial.coe_norm_unit
modified def polynomial.coeff
modified theorem polynomial.coeff_C_mul
modified theorem polynomial.coeff_C_mul_X
modified theorem polynomial.coeff_X
modified theorem polynomial.coeff_X_one
modified theorem polynomial.coeff_X_zero
modified theorem polynomial.coeff_add
modified theorem polynomial.coeff_derivative
modified theorem polynomial.coeff_inv_units
modified theorem polynomial.coeff_mk
modified theorem polynomial.coeff_mul
modified theorem polynomial.coeff_mul_X
modified theorem polynomial.coeff_mul_X_pow
modified theorem polynomial.coeff_mul_X_zero
modified theorem polynomial.coeff_neg
modified theorem polynomial.coeff_one
modified theorem polynomial.coeff_one_zero
modified theorem polynomial.coeff_smul
modified theorem polynomial.coeff_sub
modified theorem polynomial.coeff_sum
modified theorem polynomial.coeff_zero
modified def polynomial.comp
modified theorem polynomial.comp_zero
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_X_sub_C
modified theorem polynomial.degree_add_le
modified theorem polynomial.degree_coe_units
modified theorem polynomial.degree_div_le
modified theorem polynomial.degree_erase_le
modified theorem polynomial.degree_lt_wf
modified theorem polynomial.degree_map'
modified theorem polynomial.degree_map
modified theorem polynomial.degree_map_le
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_eq
modified theorem polynomial.degree_pow_le
modified theorem polynomial.degree_sum_le
modified theorem polynomial.degree_zero
modified def polynomial.derivative
modified theorem polynomial.derivative_C
modified theorem polynomial.derivative_X
modified theorem polynomial.derivative_add
modified theorem polynomial.derivative_eval
modified theorem polynomial.derivative_mul
modified theorem polynomial.derivative_one
modified theorem polynomial.derivative_sum
modified theorem polynomial.derivative_zero
modified def polynomial.div
modified def polynomial.div_X
modified theorem polynomial.div_X_C
modified theorem polynomial.div_X_mul_X_add
modified theorem polynomial.div_by_monic_one
modified def polynomial.eval
modified theorem polynomial.eval_map
modified theorem polynomial.eval_neg
modified theorem polynomial.eval_one
modified theorem polynomial.eval_sub
modified theorem polynomial.eval_sum
modified theorem polynomial.eval_zero
modified def polynomial.eval₂
modified theorem polynomial.eval₂_comp
modified theorem polynomial.eval₂_hom
modified theorem polynomial.eval₂_map
modified theorem polynomial.eval₂_neg
modified theorem polynomial.eval₂_one
modified theorem polynomial.eval₂_sub
modified theorem polynomial.eval₂_sum
modified theorem polynomial.eval₂_zero
modified theorem polynomial.ext
modified theorem polynomial.ext_iff
modified theorem polynomial.finset_sum_coeff
modified theorem polynomial.hom_eval₂
modified theorem polynomial.int_cast_eq_C
modified def polynomial.is_root
modified def polynomial.lcoeff
modified theorem polynomial.lcoeff_apply
modified theorem polynomial.leading_coeff_C
modified theorem polynomial.leading_coeff_X
modified def polynomial.map
modified theorem polynomial.map_div
modified theorem polynomial.map_div_by_monic
modified theorem polynomial.map_eq_zero
modified theorem polynomial.map_injective
modified theorem polynomial.map_map
modified theorem polynomial.map_mod
modified theorem polynomial.map_mod_by_monic
modified theorem polynomial.map_neg
modified theorem polynomial.map_one
modified theorem polynomial.map_sub
modified theorem polynomial.map_zero
modified theorem polynomial.mem_map_range
modified theorem polynomial.mem_nth_roots
modified theorem polynomial.mem_roots_sub_C
modified def polynomial.mod
modified theorem polynomial.mod_by_monic_X
modified theorem polynomial.mod_by_monic_one
modified theorem polynomial.monic.as_sum
modified theorem polynomial.monic.ne_zero
modified def polynomial.monic
modified theorem polynomial.monic_X
modified theorem polynomial.monic_X_add_C
modified theorem polynomial.monic_X_sub_C
modified theorem polynomial.monic_map
modified theorem polynomial.monic_one
modified def polynomial.monomial
modified theorem polynomial.nat_cast_eq_C
modified def polynomial.nat_degree
modified theorem polynomial.nat_degree_C
modified theorem polynomial.nat_degree_map'
modified theorem polynomial.nat_degree_map
modified theorem polynomial.nat_degree_neg
modified theorem polynomial.nat_degree_one
modified theorem polynomial.nat_degree_zero
modified theorem polynomial.not_monic_zero
modified def polynomial.nth_roots
modified theorem polynomial.one_comp
modified theorem polynomial.sum_C_mul_X_eq
modified theorem polynomial.support_zero
modified theorem polynomial.zero_comp
modified def polynomial