The set of non-invertible elements of a monoid #
Main definitions #
nonunits
is the set of non-invertible elements of a monoid.
Main results #
exists_max_ideal_of_mem_nonunits
: every element ofnonunits
is contained in a maximal ideal
theorem
exists_max_ideal_of_mem_nonunits
{α : Type u_2}
{a : α}
[CommSemiring α]
(h : a ∈ nonunits α)
: