mathlib3

69485051 - feat(data/polynomial): prime_of_degree_eq_one_of_monic (#2745)