Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-22 08:31 0e519766

View on Github →

feat(data/polynomial/reverse): Trailing degree is multiplicative (#6351) Uses polynomial.reverse to prove that nat_trailing_degree behaves well under multiplication.

Estimated changes

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

added theorem polynomial.nat_trailing_degree_le_nat_degree

Modified src/data/polynomial/reverse.lean

added theorem polynomial.coeff_reverse

added theorem polynomial.nat_degree_eq_reverse_nat_degree_add_nat_trailing_degree

added theorem polynomial.reflect_neg

added theorem polynomial.reflect_sub

added theorem polynomial.reverse_eq_zero

added theorem polynomial.reverse_leading_coeff

added theorem polynomial.reverse_nat_degree

added theorem polynomial.reverse_nat_degree_le

added theorem polynomial.reverse_nat_trailing_degree

added theorem polynomial.reverse_neg

added theorem polynomial.reverse_trailing_coeff

added theorem polynomial.trailing_coeff_mul

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.nat_trailing_degree_mul