mathlib3

c9dc8c1f - feat(src/data/polynomial/degree/definitions.lean): a lemma about monic polynomials (#15818)

feat(src/data/polynomial/degree/definitions.lean): a lemma about monic polynomials (#15818) A polynomial is monic is its degree is at most `n` and its `n`-th coefficient equals `1`. This is a lemma that `tactic.interactive.compute_degree` uses.