mathlib

2ad9b39a - feat(algebra/associated): add irreducible.not_dvd_one (#12686)