mathlib3

229cf6ef - feat(data/polynomial): irreducible_of_irreducible_mod_prime (#3539)

feat(data/polynomial): irreducible_of_irreducible_mod_prime (#3539) I was waiting on this, an exercise from Johan's tutorial at LftCM, to see if a participant would PR it. Perhaps not, so I'll contribute this now. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>