Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-18 14:10 ce990c59

View on Github →

feat(linear_algebra/univariate_polynomial): univariate polynomials

Estimated changes

Modified data/finset.lean

added theorem finset.max_eq_none

added theorem finset.min_eq_none

Created linear_algebra/univariate_polynomial.lean

added def polynomial.C

added theorem polynomial.C_0

added theorem polynomial.C_1

added theorem polynomial.C_apply

added theorem polynomial.C_apply_zero

added theorem polynomial.C_mul_C

added theorem polynomial.C_mul_apply

added theorem polynomial.C_mul_monomial

added def polynomial.X

added theorem polynomial.X_apply_one

added theorem polynomial.X_pow_eq_monomial

added theorem polynomial.add_apply

added theorem polynomial.card_roots

added def polynomial.degree

added theorem polynomial.degree_C

added theorem polynomial.degree_X

added theorem polynomial.degree_X_sub_C

added theorem polynomial.degree_add_div_by_monic

added theorem polynomial.degree_add_eq_of_degree_lt

added theorem polynomial.degree_add_eq_of_leading_coeff_add_ne_zero

added theorem polynomial.degree_add_le

added theorem polynomial.degree_div_by_monic_le

added theorem polynomial.degree_div_by_monic_lt

added theorem polynomial.degree_eq_bot

added theorem polynomial.degree_eq_nat_degree

added theorem polynomial.degree_erase_le

added theorem polynomial.degree_erase_lt

added def polynomial.degree_lt_wf

added theorem polynomial.degree_mod_by_monic_lt

added theorem polynomial.degree_monomial

added theorem polynomial.degree_monomial_le

added theorem polynomial.degree_mul_eq'

added theorem polynomial.degree_mul_eq

added theorem polynomial.degree_mul_le

added theorem polynomial.degree_mul_leading_coeff_inv

added theorem polynomial.degree_neg

added theorem polynomial.degree_one

added theorem polynomial.degree_pos_of_root

added theorem polynomial.degree_pow_eq'

added theorem polynomial.degree_pow_eq

added theorem polynomial.degree_pow_le

added theorem polynomial.degree_sub_lt

added theorem polynomial.degree_sum_le

added theorem polynomial.degree_zero

added def polynomial.div

added def polynomial.div_by_monic

added theorem polynomial.div_by_monic_eq_div

added theorem polynomial.div_by_monic_eq_of_not_monic

added theorem polynomial.div_by_monic_eq_zero_iff

added theorem polynomial.div_by_monic_zero

added def polynomial.div_mod_by_monic_aux

added theorem polynomial.div_wf_lemma

added theorem polynomial.dvd_iff_mod_by_monic_eq_zero

added theorem polynomial.eq_C_of_degree_le_zero

added theorem polynomial.eq_zero_of_degree_lt

added def polynomial.eval

added theorem polynomial.eval_C

added theorem polynomial.eval_X

added theorem polynomial.eval_add

added theorem polynomial.eval_monomial

added theorem polynomial.eval_mul

added theorem polynomial.eval_mul_monomial

added theorem polynomial.eval_neg

added theorem polynomial.eval_sub

added theorem polynomial.eval_zero

added theorem polynomial.exists_finset_roots

added theorem polynomial.induction_on

added theorem polynomial.is_root.def

added def polynomial.is_root

added theorem polynomial.le_degree_of_ne_zero

added def polynomial.leading_coeff

added theorem polynomial.leading_coeff_C

added theorem polynomial.leading_coeff_X

added theorem polynomial.leading_coeff_add_of_degree_eq

added theorem polynomial.leading_coeff_add_of_degree_lt

added theorem polynomial.leading_coeff_eq_zero

added theorem polynomial.leading_coeff_monomial

added theorem polynomial.leading_coeff_mul'

added theorem polynomial.leading_coeff_mul

added theorem polynomial.leading_coeff_one

added theorem polynomial.leading_coeff_pow'

added theorem polynomial.leading_coeff_pow

added theorem polynomial.leading_coeff_zero

added theorem polynomial.mem_roots

added def polynomial.mod

added theorem polynomial.mod_X_sub_C_eq_C_eval

added def polynomial.mod_by_monic

added theorem polynomial.mod_by_monic_X_sub_C_eq_C_eval

added theorem polynomial.mod_by_monic_add_div

added theorem polynomial.mod_by_monic_eq_mod

added theorem polynomial.mod_by_monic_eq_of_not_monic

added theorem polynomial.mod_by_monic_eq_self_iff

added theorem polynomial.mod_by_monic_eq_sub_mul_div

added theorem polynomial.mod_by_monic_zero

added theorem polynomial.monic.def

added def polynomial.monic

added theorem polynomial.monic_X_sub_C

added theorem polynomial.monic_mul_leading_coeff_inv

added theorem polynomial.monic_one

added def polynomial.monomial

added theorem polynomial.monomial_add_left

added theorem polynomial.monomial_add_right

added theorem polynomial.monomial_apply

added theorem polynomial.monomial_apply_self

added theorem polynomial.monomial_eq

added theorem polynomial.monomial_induction_on

added theorem polynomial.monomial_mul_monomial

added theorem polynomial.monomial_zero_right

added theorem polynomial.mul_apply_degree_add_degree

added theorem polynomial.mul_div_by_monic_eq_iff_is_root

added theorem polynomial.mul_div_eq_iff_is_root

added def polynomial.nat_degree

added theorem polynomial.nat_degree_C

added theorem polynomial.nat_degree_eq_of_degree_eq

added theorem polynomial.nat_degree_mul_eq'

added theorem polynomial.ne_zero_of_degree_gt

added theorem polynomial.ne_zero_of_monic

added theorem polynomial.ne_zero_of_ne_zero_of_monic

added theorem polynomial.neg_apply

added theorem polynomial.not_monic_zero

added theorem polynomial.one_apply_zero

added theorem polynomial.root_X_sub_C

added theorem polynomial.root_mul_left_of_is_root

added theorem polynomial.root_mul_right_of_is_root

added theorem polynomial.root_or_root_of_root_mul

added theorem polynomial.subsingleton_of_monic_zero

added theorem polynomial.support_zero

added theorem polynomial.zero_apply

added theorem polynomial.zero_div_by_monic

added theorem polynomial.zero_mod_by_monic

added def polynomial

added theorem with_bot.add_bot

added theorem with_bot.bot_add

added theorem with_bot.bot_lt_some

added theorem with_bot.coe_add

added theorem with_bot.coe_lt_coe

Modified order/bounded_lattice.lean

added theorem with_bot.well_founded_lt

added theorem with_top.well_founded_lt