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 of nonunits is contained in a maximal ideal

def nonunits (α : Type u_4) [Monoid α] : Set α

The set of non-invertible elements of a monoid.

@[simp]

theorem mem_nonunits_iff {α : Type u_2} {a : α} [Monoid α] : a ∈ nonunits α ↔ ¬IsUnit a

theorem mul_mem_nonunits_right {α : Type u_2} {a b : α} [CommMonoid α] : b ∈ nonunits α → a * b ∈ nonunits α

theorem mul_mem_nonunits_left {α : Type u_2} {a b : α} [CommMonoid α] : a ∈ nonunits α → a * b ∈ nonunits α

theorem zero_mem_nonunits {α : Type u_2} [MonoidWithZero α] : 0 ∈ nonunits α ↔ 0 ≠ 1

@[simp]

theorem one_notMem_nonunits {α : Type u_2} [Monoid α] : 1 ∉ nonunits α

@[deprecated one_notMem_nonunits (since := "2025-05-23")]

theorem one_not_mem_nonunits {α : Type u_2} [Monoid α] : 1 ∉ nonunits α

Alias of one_notMem_nonunits.

@[simp]

theorem map_mem_nonunits_iff {F : Type u_1} {α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a : α) : f a ∈ nonunits β ↔ a ∈ nonunits α

theorem coe_subset_nonunits {α : Type u_2} [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : ↑I ⊆ nonunits α

theorem exists_max_ideal_of_mem_nonunits {α : Type u_2} {a : α} [CommSemiring α] (h : a ∈ nonunits α) : ∃ (I : Ideal α), I.IsMaximal ∧ a ∈ I