mathlib3

b353d8e9 - chore(data/polynomial/degree/lemmas): rename lemmas that should have been renamed in an earlier PR (#15819)

chore(data/polynomial/degree/lemmas): rename lemmas that should have been renamed in an earlier PR (#15819) In #15694 I was asked to modify some of these lemmas, but forgot to update their names to their new statements. This PR corrects this oversight.