feat(algebra/associated): Primes that divide each other are associated (#6732)
feat(algebra/associated): Primes that divide each other are associated (#6732)

Primes that divide each other are associated






leanprover-community/mathlib,leanprover-community/mathlib