mathlib3

9d54837a - feat(data/polynomial/degree): lemmas on nat_degree and behaviour under multiplication by constants (#6224)

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