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 α

@[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

theorem Submonoid.inv_mem_of_isUnit {α : Type u_2} {C : Type u_4} [SetLike C α] [DivisionMonoid α] [SubmonoidClass C α] {S : C} {a : ↥S} (ha : IsUnit a) : (↑a)⁻¹ ∈ S

theorem Submonoid.isUnit_iff {α : Type u_2} {C : Type u_4} [SetLike C α] [Group α] [SubmonoidClass C α] {S : C} {a : ↥S} : IsUnit a ↔ (↑a)⁻¹ ∈ S

theorem Submonoid.mem_nonunits_iff {α : Type u_2} {C : Type u_4} [SetLike C α] [Group α] [SubmonoidClass C α] {S : C} {a : ↥S} : a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S

theorem Submonoid.isUnit_iff_and {α : Type u_2} {C : Type u_4} [SetLike C α] [GroupWithZero α] [SubmonoidClass C α] {S : C} {a : ↥S} : IsUnit a ↔ ↑a ≠ 0 ∧ (↑a)⁻¹ ∈ S

theorem Submonoid.isUnit_iff_of_ne_zero {α : Type u_2} {C : Type u_4} [SetLike C α] [GroupWithZero α] [SubmonoidClass C α] {S : C} {a : ↥S} (ha : ↑a ≠ 0) : IsUnit a ↔ (↑a)⁻¹ ∈ S

theorem Submonoid.mem_nonunits_iff_or {α : Type u_2} {C : Type u_4} [SetLike C α] [GroupWithZero α] [SubmonoidClass C α] {S : C} {a : ↥S} : a ∈ nonunits ↥S ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S

theorem Submonoid.mem_nonunits_iff_of_ne_zero {α : Type u_2} {C : Type u_4} [SetLike C α] [GroupWithZero α] [SubmonoidClass C α] {S : C} {a : ↥S} (ha : ↑a ≠ 0) : a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S