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.

instance Associates.instOrderedCommMonoid {M : Type u_1} [CancelCommMonoidWithZero M] : OrderedCommMonoid (Associates M)

Equations

• Associates.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Associates.instCanonicallyOrderedCommMonoid {M : Type u_1} [CancelCommMonoidWithZero M] : CanonicallyOrderedCommMonoid (Associates M)

Equations

• Associates.instCanonicallyOrderedCommMonoid = CanonicallyOrderedCommMonoid.mk ⋯ ⋯