mathlib3

26729d6d - chore(ring_theory/polynomial/basic): Generalize `polynomial.degree_lt_equiv` to commutative rings (#13190)

chore(ring_theory/polynomial/basic): Generalize `polynomial.degree_lt_equiv` to commutative rings (#13190) This is a minor PR to generalise degree_lt_equiv to comm_ring. Its restriction to field appears to be an oversight. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>