Module docstring
{"# Submonoid of primal elements "}
Submonoid.isPrimal
definition
(M₀ : Type*) [CancelCommMonoidWithZero M₀] : Submonoid M₀
Full source
/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
def Submonoid.isPrimal (M₀ : Type*) [CancelCommMonoidWithZero M₀] : Submonoid M₀ where
carrier := {a | IsPrimal a}
mul_mem' := .mul
one_mem' := isUnit_one.isPrimalInformal description
The submonoid of primal elements in a cancellative commutative monoid with zero $M_0$ consists of all elements $a \in M_0$ that are primal, i.e., for any $b, c \in M_0$ such that $a$ divides $b \cdot c$, there exist $a_1, a_2 \in M_0$ with $a_1$ dividing $b$, $a_2$ dividing $c$, and $a = a_1 \cdot a_2$. This submonoid is closed under multiplication and contains the multiplicative identity.