# Associated, prime, and irreducible elements. #

In this file we define the predicate `Prime p`

saying that an element of a commutative monoid with zero is prime.
Namely, `Prime p`

means that `p`

isn't zero, it isn't a unit,
and `p ∣ a * b → p ∣ a ∨ p ∣ b`

for all `a`

, `b`

;

In decomposition monoids (e.g., `ℕ`

, `ℤ`

), this predicate is equivalent to `Irreducible`

,
however this is not true in general.

We also define an equivalence relation `Associated`

saying that two elements of a monoid differ by a multiplication by a unit.
Then we show that the quotient type `Associates`

is a monoid
and prove basic properties of this quotient.

## Equations

- Associates.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

## Equations

- Associates.instCanonicallyOrderedCommMonoid = CanonicallyOrderedCommMonoid.mk ⋯ ⋯