mathlib

2d76f563 - chore(algebra/associated): make `irreducible` not a class (#14713)

chore(algebra/associated): make `irreducible` not a class (#14713) This functionality was rarely used and doesn't align with how `irreducible` is used in practice. In a future PR, we can remove some `unfreezingI`s caused by this. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>