Submonoid of primal elements

def Submonoid.isPrimal (M₀ : Type u_1) [CancelCommMonoidWithZero M₀] : Submonoid M₀

The submonoid of primal elements in a cancellative commutative monoid with zero.

Equations

• Submonoid.isPrimal M₀ = { carrier := {a : M₀ | IsPrimal a}, mul_mem' := ⋯, one_mem' := ⋯ }