Associated, prime, and irreducible elements. #
prime element of a CommMonoidWithZero
Instances For
p
is not a unitif
p
factors then one factor is a unit
Irreducible p
states that p
is non-unit and only factors into units.
We explicitly avoid stating that p
is non-zero, this would require a semiring. Assuming only a
monoid allows us to reuse irreducible for associated elements.
Instances For
If p
and q
are irreducible, then p ∣ q
implies q ∣ p
.
Two elements of a Monoid
are Associated
if one of them is another one
multiplied by a unit on the right.
Instances For
The setoid of the relation x ~ᵤ y
iff there is a unit u
such that x * u = y
Instances For
The quotient of a monoid by the Associated
relation. Two elements x
and y
are associated iff there is a unit u
such that x * u = y
. There is a natural
monoid structure on Associates α
.
Instances For
The canonical quotient map from a monoid α
into the Associates
of α
Instances For
Associates.mk
as a MonoidHom
.