mathlib3

d42f6a82 - chore(algebra/associated): golf irreducible_iff_prime_iff (#13267)