Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-24 13:04 229cf6ef

View on Github →

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.

Estimated changes