Commit 2021-02-22 14:12 9d54837a

View on Github →

feat(data/polynomial/degree): lemmas on nat_degree and behaviour under multiplication by constants (#6224) These lemmas extend the API for nat_degree I intend to use them to work with integrality statements

Estimated changes

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

modified theorem polynomial.eq_C_of_nat_degree_eq_zero

modified theorem polynomial.eq_C_of_nat_degree_le_zero

modified theorem polynomial.le_nat_degree_of_coe_le_degree

added theorem polynomial.leading_coeff_ne_zero

modified theorem polynomial.nat_degree_pos_iff_degree_pos

modified theorem polynomial.ne_zero_of_coe_le_degree

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

added theorem polynomial.eq_nat_degree_of_le_mem_support

added theorem polynomial.nat_degree_C_mul_eq_of_mul_eq_one

added theorem polynomial.nat_degree_C_mul_eq_of_mul_ne_zero

added theorem polynomial.nat_degree_C_mul_eq_of_no_zero_divisors

added theorem polynomial.nat_degree_C_mul_le

added theorem polynomial.nat_degree_add_coeff_mul

added theorem polynomial.nat_degree_le_iff_coeff_eq_zero

added theorem polynomial.nat_degree_lt_coeff_mul

added theorem polynomial.nat_degree_mul_C_eq_of_mul_eq_one

added theorem polynomial.nat_degree_mul_C_eq_of_mul_ne_zero

added theorem polynomial.nat_degree_mul_C_eq_of_no_zero_divisors

added theorem polynomial.nat_degree_mul_C_le