mathlib3

af4c6c8a - chore(ring_theory/polynomial/basic): golf polynomial_not_is_field (#13919)