Documentation

Mathlib.RingTheory.Ideal.Nonunits

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.

Equations

nonunits α = {a : α | ¬IsUnit a}

Instances For

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

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