Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-18 16:49 4760a33a

View on Github →

feat(algebra/polynomial, data/polynomial): lemmas about monic polynomials (#3402)

Estimated changes

Modified src/algebra/char_p.lean

added theorem add_pow_char_of_commute

Deleted src/algebra/polynomial/basic.lean

deleted theorem polynomial.coe_aeval_eq_eval

deleted theorem polynomial.coeff_zero_eq_aeval_zero

deleted def polynomial.leading_coeff_hom

deleted theorem polynomial.leading_coeff_hom_apply

Modified src/algebra/polynomial/big_operators.lean

deleted theorem polynomial.monic_prod_of_monic

added theorem polynomial.nat_degree_prod'

added theorem polynomial.nat_degree_prod

deleted theorem polynomial.nat_degree_prod_eq'

deleted theorem polynomial.nat_degree_prod_eq

deleted theorem polynomial.nat_degree_prod_eq_of_monic

added theorem polynomial.nat_degree_prod_of_monic

added theorem polynomial.prod_X_sub_C_coeff_card_pred

added theorem polynomial.prod_X_sub_C_next_coeff

Modified src/data/polynomial/algebra_map.lean

added theorem polynomial.coe_aeval_eq_eval

added theorem polynomial.coeff_zero_eq_aeval_zero

added theorem polynomial.pow_comp

Modified src/data/polynomial/degree.lean

added theorem polynomial.degree_mul'

added theorem polynomial.degree_mul

deleted theorem polynomial.degree_mul_eq'

added theorem polynomial.degree_pow'

added theorem polynomial.degree_pow

deleted theorem polynomial.degree_pow_eq'

added def polynomial.leading_coeff_hom

added theorem polynomial.leading_coeff_hom_apply

added theorem polynomial.leading_coeff_mul

added theorem polynomial.leading_coeff_pow

added theorem polynomial.nat_degree_mul'

deleted theorem polynomial.nat_degree_mul_eq'

added theorem polynomial.nat_degree_pow'

deleted theorem polynomial.nat_degree_pow_eq'

added theorem polynomial.next_coeff_X_sub_C

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

added def polynomial.next_coeff

added theorem polynomial.next_coeff_C_eq_zero

added theorem polynomial.next_coeff_of_pos_nat_degree

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/field_division.lean

Modified src/data/polynomial/monic.lean

added theorem polynomial.monic.coeff_nat_degree

added theorem polynomial.monic.degree_eq_zero_iff_eq_one

added theorem polynomial.monic.nat_degree_mul

added theorem polynomial.monic.next_coeff_mul

added theorem polynomial.monic.next_coeff_prod

added theorem polynomial.monic_prod_of_monic

Modified src/data/polynomial/ring_division.lean

deleted theorem polynomial.degree_mul_eq

deleted theorem polynomial.degree_pow_eq

deleted theorem polynomial.leading_coeff_mul

deleted theorem polynomial.leading_coeff_pow

added theorem polynomial.nat_degree_mul

deleted theorem polynomial.nat_degree_mul_eq

added theorem polynomial.nat_degree_pow

deleted theorem polynomial.nat_degree_pow_eq

Modified src/linear_algebra/lagrange.lean

Modified src/ring_theory/eisenstein_criterion.lean

Modified src/ring_theory/polynomial/basic.lean