reverse): Trailing degree is multiplicative (#6351)

Commit

4 years ago

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

Author

tb65536

Parents

a3d951bc

mathlib3 0e519766 - feat(data/polynomial/reverse): Trailing degree is multiplicative (#6351)

mathlib3
0e519766 - feat(data/polynomial/reverse): Trailing degree is multiplicative (#6351)