Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-27 19:53 97065dbf

View on Github →

refactor(data/polynomial): use linear_map for monomial, review degree (#4784)

Estimated changes

Modified src/algebra/algebra/basic.lean

added theorem alg_hom.map_int_cast

Modified src/algebra/group/basic.lean

added theorem one_eq_inv

Modified src/analysis/calculus/deriv.lean

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/basic.lean

modified def polynomial.monomial

added theorem polynomial.monomial_def

modified theorem polynomial.monomial_zero_right

added theorem polynomial.smul_monomial

Modified src/data/polynomial/degree.lean

deleted theorem polynomial.eq_C_of_nat_degree_eq_zero

Modified src/data/polynomial/degree/basic.lean

modified theorem polynomial.C_eq_int_cast

added theorem polynomial.as_sum_range_C_mul_X_pow

added theorem polynomial.as_sum_support_C_mul_X_pow

added theorem polynomial.coeff_nat_degree

added theorem polynomial.degree_C_mul_X_pow

modified theorem polynomial.degree_C_mul_X_pow_le

modified theorem polynomial.degree_X_pow

modified theorem polynomial.degree_monomial

modified theorem polynomial.degree_monomial_le

added theorem polynomial.eq_C_of_nat_degree_eq_zero

added theorem polynomial.eq_X_add_C_of_nat_degree_le_one

added theorem polynomial.exists_eq_X_add_C_of_nat_degree_le_one

modified theorem polynomial.mem_support_C_mul_X_pow

added theorem polynomial.monic.ne_zero_of_ne

added theorem polynomial.monic.ne_zero_of_polynomial_ne

deleted theorem polynomial.monic.ne_zero_of_zero_ne_one

modified theorem polynomial.nat_degree_C_mul_X_pow_of_nonzero

added theorem polynomial.nat_degree_le_iff_degree_le

deleted theorem polynomial.nat_degree_le_of_degree_le

added theorem polynomial.supp_subset_range

modified theorem polynomial.support_C_mul_X_pow_nonzero

Modified src/data/polynomial/degree/trailing_degree.lean

modified theorem polynomial.le_trailing_degree_C_mul_X_pow

added theorem polynomial.le_trailing_degree_monomial

deleted theorem polynomial.monomial_le_trailing_degree

added theorem polynomial.nat_trailing_degree_monomial

added theorem polynomial.nat_trailing_degree_monomial_le

added theorem polynomial.trailing_degree_C_mul_X_pow

modified theorem polynomial.trailing_degree_monomial

Modified src/data/polynomial/derivative.lean

added theorem polynomial.derivative_C_mul_X_pow

modified theorem polynomial.derivative_monomial

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/erase_lead.lean

Modified src/data/polynomial/eval.lean

Modified src/data/polynomial/field_division.lean

Modified src/data/polynomial/monic.lean

Modified src/data/polynomial/monomial.lean

added theorem polynomial.nontrivial.of_polynomial_ne

deleted theorem polynomial.nonzero.of_polynomial_ne

Modified src/data/real/irrational.lean

deleted theorem nat_degree_gt_one_of_irrational_root

added theorem one_lt_nat_degree_of_irrational_root

Modified src/field_theory/separable.lean

Modified src/ring_theory/polynomial/basic.lean

Modified src/ring_theory/polynomial/scale_roots.lean

Modified src/ring_theory/polynomial_algebra.lean

added theorem poly_equiv_tensor.inv_fun_monomial