Documentation

Mathlib.Algebra.GroupWithZero.Submonoid.Primal

Submonoid of primal elements #

def Submonoid.isPrimal (Mâ‚€ : Type u_1) [CommMonoidWithZero Mâ‚€] [IsCancelMulZero Mâ‚€] :
Submonoid Mâ‚€

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

Equations
    Instances For