Ideals over a ring

This file defines Ideal R, the type of (left) ideals over a ring R. Note that over commutative rings, left ideals and two-sided ideals are equivalent.

Implementation notes

Ideal R is implemented using Submodule R R, where • is interpreted as *.

TODO

Support right ideals, and two-sided ideals over non-commutative rings.

@[reducible]

def Ideal (R : Type u) [Semiring R] : Type u

A (left) ideal in a semiring R is an additive submonoid s such that a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.

Equations

• Ideal R = Submodule R R

theorem Ideal.zero_mem {α : Type u} [Semiring α] (I : Ideal α) : 0 ∈ I

theorem Ideal.add_mem {α : Type u} [Semiring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → b ∈ I → a + b ∈ I

theorem Ideal.mul_mem_left {α : Type u} [Semiring α] (I : Ideal α) (a : α) {b : α} : b ∈ I → a * b ∈ I

theorem Ideal.ext {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (h : ∀ (x : α), x ∈ I ↔ x ∈ J) : I = J

theorem Ideal.sum_mem {α : Type u} [Semiring α] (I : Ideal α) {ι : Type u_1} {t : Finset ι} {f : ι → α} : (∀ c ∈ t, f c ∈ I) → (Finset.sum t fun (i : ι) => f i) ∈ I

theorem Ideal.eq_top_of_unit_mem {α : Type u} [Semiring α] (I : Ideal α) (x : α) (y : α) (hx : x ∈ I) (h : y * x = 1) : I = ⊤

theorem Ideal.eq_top_of_isUnit_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} (hx : x ∈ I) (h : IsUnit x) : I = ⊤

theorem Ideal.eq_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) : I = ⊤ ↔ 1 ∈ I

theorem Ideal.ne_top_iff_one {α : Type u} [Semiring α] (I : Ideal α) : I ≠ ⊤ ↔ 1 ∉ I

@[simp]

theorem Ideal.unit_mul_mem_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) : y * x ∈ I ↔ x ∈ I

def Ideal.span {α : Type u} [Semiring α] (s : Set α) : Ideal α

The ideal generated by a subset of a ring

Equations

• Ideal.span s = Submodule.span α s

@[simp]

theorem Ideal.submodule_span_eq {α : Type u} [Semiring α] {s : Set α} : Submodule.span α s = Ideal.span s

@[simp]

theorem Ideal.span_empty {α : Type u} [Semiring α] : Ideal.span ∅ = ⊥

@[simp]

theorem Ideal.span_univ {α : Type u} [Semiring α] : Ideal.span Set.univ = ⊤

theorem Ideal.span_union {α : Type u} [Semiring α] (s : Set α) (t : Set α) : Ideal.span (s ∪ t) = Ideal.span s ⊔ Ideal.span t

theorem Ideal.span_iUnion {α : Type u} [Semiring α] {ι : Sort u_1} (s : ι → Set α) : Ideal.span (⋃ (i : ι), s i) = ⨆ (i : ι), Ideal.span (s i)

theorem Ideal.mem_span {α : Type u} [Semiring α] {s : Set α} (x : α) : x ∈ Ideal.span s ↔ ∀ (p : Ideal α), s ⊆ ↑p → x ∈ p

theorem Ideal.subset_span {α : Type u} [Semiring α] {s : Set α} : s ⊆ ↑(Ideal.span s)

theorem Ideal.span_le {α : Type u} [Semiring α] {s : Set α} {I : Ideal α} : Ideal.span s ≤ I ↔ s ⊆ ↑I

theorem Ideal.span_mono {α : Type u} [Semiring α] {s : Set α} {t : Set α} : s ⊆ t → Ideal.span s ≤ Ideal.span t

@[simp]

theorem Ideal.span_eq {α : Type u} [Semiring α] (I : Ideal α) : Ideal.span ↑I = I

@[simp]

theorem Ideal.span_singleton_one {α : Type u} [Semiring α] : Ideal.span {1} = ⊤

theorem Ideal.isCompactElement_top {α : Type u} [Semiring α] : CompleteLattice.IsCompactElement ⊤

theorem Ideal.mem_span_insert {α : Type u} [Semiring α] {s : Set α} {x : α} {y : α} : x ∈ Ideal.span (insert y s) ↔ ∃ (a : α), ∃ z ∈ Ideal.span s, x = a * y + z

theorem Ideal.mem_span_singleton' {α : Type u} [Semiring α] {x : α} {y : α} : x ∈ Ideal.span {y} ↔ ∃ (a : α), a * y = x

theorem Ideal.span_singleton_le_iff_mem {α : Type u} [Semiring α] (I : Ideal α) {x : α} : Ideal.span {x} ≤ I ↔ x ∈ I

theorem Ideal.span_singleton_mul_left_unit {α : Type u} [Semiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {a * x} = Ideal.span {x}

theorem Ideal.span_insert {α : Type u} [Semiring α] (x : α) (s : Set α) : Ideal.span (insert x s) = Ideal.span {x} ⊔ Ideal.span s

theorem Ideal.span_eq_bot {α : Type u} [Semiring α] {s : Set α} : Ideal.span s = ⊥ ↔ ∀ x ∈ s, x = 0

@[simp]

theorem Ideal.span_singleton_eq_bot {α : Type u} [Semiring α] {x : α} : Ideal.span {x} = ⊥ ↔ x = 0

theorem Ideal.span_singleton_ne_top {α : Type u_1} [CommSemiring α] {x : α} (hx : ¬IsUnit x) : Ideal.span {x} ≠ ⊤

@[simp]

theorem Ideal.span_zero {α : Type u} [Semiring α] : Ideal.span 0 = ⊥

@[simp]

theorem Ideal.span_one {α : Type u} [Semiring α] : Ideal.span 1 = ⊤

theorem Ideal.span_eq_top_iff_finite {α : Type u} [Semiring α] (s : Set α) : Ideal.span s = ⊤ ↔ ∃ (s' : Finset α), ↑s' ⊆ s ∧ Ideal.span ↑s' = ⊤

theorem Ideal.mem_span_singleton_sup {S : Type u_1} [CommSemiring S] {x : S} {y : S} {I : Ideal S} : x ∈ Ideal.span {y} ⊔ I ↔ ∃ (a : S), ∃ b ∈ I, a * y + b = x

def Ideal.ofRel {α : Type u} [Semiring α] (r : α → α → Prop) : Ideal α

The ideal generated by an arbitrary binary relation.

Equations

• Ideal.ofRel r = Submodule.span α {x : α | ∃ (a : α) (b : α) (_ : r a b), x + b = a}

class Ideal.IsPrime {α : Type u} [Semiring α] (I : Ideal α) : Prop

An ideal P of a ring R is prime if P ≠ R and xy ∈ P → x ∈ P ∨ y ∈ P

• ne_top' : I ≠ ⊤

  The prime ideal is not the entire ring.

• mem_or_mem' : ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

  If a product lies in the prime ideal, then at least one element lies in the prime ideal.

theorem Ideal.isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.ne_top {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) : I ≠ ⊤

theorem Ideal.IsPrime.mem_or_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} : x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mem_or_mem_of_mul_eq_zero {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} (h : x * y = 0) : x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.mem_of_pow_mem {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I

theorem Ideal.not_isPrime_iff {α : Type u} [Semiring α] {I : Ideal α} : ¬Ideal.IsPrime I ↔ I = ⊤ ∨ ∃ (x : α) (_ : x ∉ I) (y : α) (_ : y ∉ I), x * y ∈ I

theorem Ideal.zero_ne_one_of_proper {α : Type u} [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : 0 ≠ 1

theorem Ideal.bot_prime {α : Type u} [Semiring α] [IsDomain α] : Ideal.IsPrime ⊥

class Ideal.IsMaximal {α : Type u} [Semiring α] (I : Ideal α) : Prop

An ideal is maximal if it is maximal in the collection of proper ideals.

• out : IsCoatom I

  The maximal ideal is a coatom in the ordering on ideals; that is, it is not the entire ring, and there are no other proper ideals strictly containing it.

theorem Ideal.isMaximal_def {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsMaximal I ↔ IsCoatom I

theorem Ideal.IsMaximal.ne_top {α : Type u} [Semiring α] {I : Ideal α} (h : Ideal.IsMaximal I) : I ≠ ⊤

theorem Ideal.isMaximal_iff {α : Type u} [Semiring α] {I : Ideal α} : Ideal.IsMaximal I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

theorem Ideal.IsMaximal.eq_of_le {α : Type u} [Semiring α] {I : Ideal α} {J : Ideal α} (hI : Ideal.IsMaximal I) (hJ : J ≠ ⊤) (IJ : I ≤ J) : I = J

instance Ideal.instIsCoatomicIdealToPartialOrderInstOmegaCompletePartialOrderCompleteLatticeToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToModuleInstOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike {α : Type u} [Semiring α] : IsCoatomic (Ideal α)

Equations

• (_ : IsCoatomic (Ideal α)) = (_ : IsCoatomic (Ideal α))

theorem Ideal.IsMaximal.coprime_of_ne {α : Type u} [Semiring α] {M : Ideal α} {M' : Ideal α} (hM : Ideal.IsMaximal M) (hM' : Ideal.IsMaximal M') (hne : M ≠ M') : M ⊔ M' = ⊤

theorem Ideal.exists_le_maximal {α : Type u} [Semiring α] (I : Ideal α) (hI : I ≠ ⊤) : ∃ (M : Ideal α), Ideal.IsMaximal M ∧ I ≤ M

Krull's theorem: if I is an ideal that is not the whole ring, then it is included in some maximal ideal.

theorem Ideal.exists_maximal (α : Type u) [Semiring α] [Nontrivial α] : ∃ (M : Ideal α), Ideal.IsMaximal M

Krull's theorem: a nontrivial ring has a maximal ideal.

instance Ideal.instNontrivialIdeal {α : Type u} [Semiring α] [Nontrivial α] : Nontrivial (Ideal α)

Equations

• (_ : Nontrivial (Ideal α)) = (_ : Nontrivial (Ideal α))

theorem Ideal.maximal_of_no_maximal {α : Type u} [Semiring α] {P : Ideal α} (hmax : ∀ (m : Ideal α), P < m → ¬Ideal.IsMaximal m) (J : Ideal α) (hPJ : P < J) : J = ⊤

If P is not properly contained in any maximal ideal then it is not properly contained in any proper ideal

theorem Ideal.span_pair_comm {α : Type u} [Semiring α] {x : α} {y : α} : Ideal.span {x, y} = Ideal.span {y, x}

theorem Ideal.mem_span_pair {α : Type u} [Semiring α] {x : α} {y : α} {z : α} : z ∈ Ideal.span {x, y} ↔ ∃ (a : α) (b : α), a * x + b * y = z

@[simp]

theorem Ideal.span_pair_add_mul_left {R : Type u} [CommRing R] {x : R} {y : R} (z : R) : Ideal.span {x + y * z, y} = Ideal.span {x, y}

@[simp]

theorem Ideal.span_pair_add_mul_right {R : Type u} [CommRing R] {x : R} {y : R} (z : R) : Ideal.span {x, y + x * z} = Ideal.span {x, y}

theorem Ideal.IsMaximal.exists_inv {α : Type u} [Semiring α] {I : Ideal α} (hI : Ideal.IsMaximal I) {x : α} (hx : x ∉ I) : ∃ (y : α), ∃ i ∈ I, y * x + i = 1

theorem Ideal.mem_sup_left {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} : x ∈ S → x ∈ S ⊔ T

theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} : x ∈ T → x ∈ S ⊔ T

theorem Ideal.mem_iSup_of_mem {R : Type u} [Semiring R] {ι : Sort u_1} {S : ι → Ideal R} (i : ι) {x : R} : x ∈ S i → x ∈ iSup S

theorem Ideal.mem_sSup_of_mem {R : Type u} [Semiring R] {S : Set (Ideal R)} {s : Ideal R} (hs : s ∈ S) {x : R} : x ∈ s → x ∈ sSup S

theorem Ideal.mem_sInf {R : Type u} [Semiring R] {s : Set (Ideal R)} {x : R} : x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I

@[simp]

theorem Ideal.mem_inf {R : Type u} [Semiring R] {I : Ideal R} {J : Ideal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

@[simp]

theorem Ideal.mem_iInf {R : Type u} [Semiring R] {ι : Sort u_1} {I : ι → Ideal R} {x : R} : x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i

@[simp]

theorem Ideal.mem_bot {R : Type u} [Semiring R] {x : R} : x ∈ ⊥ ↔ x = 0

def Ideal.pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) : Ideal (ι → α)

I^n as an ideal of R^n.

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.mem_pi {α : Type u} [Semiring α] (I : Ideal α) (ι : Type v) (x : ι → α) : x ∈ Ideal.pi I ι ↔ ∀ (i : ι), x i ∈ I

theorem Ideal.sInf_isPrime_of_isChain {α : Type u} [Semiring α] {s : Set (Ideal α)} (hs : Set.Nonempty s) (hs' : IsChain (fun (x x_1 : Ideal α) => x ≤ x_1) s) (H : ∀ p ∈ s, Ideal.IsPrime p) : Ideal.IsPrime (sInf s)

@[simp]

theorem Ideal.mul_unit_mem_iff_mem {α : Type u} [CommSemiring α] (I : Ideal α) {x : α} {y : α} (hy : IsUnit y) : x * y ∈ I ↔ x ∈ I

theorem Ideal.mem_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} : x ∈ Ideal.span {y} ↔ y ∣ x

theorem Ideal.mem_span_singleton_self {α : Type u} [CommSemiring α] (x : α) : x ∈ Ideal.span {x}

theorem Ideal.span_singleton_le_span_singleton {α : Type u} [CommSemiring α] {x : α} {y : α} : Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x

theorem Ideal.span_singleton_eq_span_singleton {α : Type u} [CommRing α] [IsDomain α] {x : α} {y : α} : Ideal.span {x} = Ideal.span {y} ↔ Associated x y

theorem Ideal.span_singleton_mul_right_unit {α : Type u} [CommSemiring α] {a : α} (h2 : IsUnit a) (x : α) : Ideal.span {x * a} = Ideal.span {x}

@[simp]

theorem Ideal.span_singleton_eq_top {α : Type u} [CommSemiring α] {x : α} : Ideal.span {x} = ⊤ ↔ IsUnit x

theorem Ideal.span_singleton_prime {α : Type u} [CommSemiring α] {p : α} (hp : p ≠ 0) : Ideal.IsPrime (Ideal.span {p}) ↔ Prime p

theorem Ideal.IsMaximal.isPrime {α : Type u} [CommSemiring α] {I : Ideal α} (H : Ideal.IsMaximal I) : Ideal.IsPrime I

instance Ideal.IsMaximal.isPrime' {α : Type u} [CommSemiring α] (I : Ideal α) [_H : Ideal.IsMaximal I] : Ideal.IsPrime I

Equations

• (_ : ∀ [_H : Ideal.IsMaximal I], Ideal.IsPrime I) = (_ : Ideal.IsMaximal I → Ideal.IsPrime I)

theorem Ideal.span_singleton_lt_span_singleton {α : Type u} [CommSemiring α] [IsDomain α] {x : α} {y : α} : Ideal.span {x} < Ideal.span {y} ↔ DvdNotUnit y x

theorem Ideal.factors_decreasing {α : Type u} [CommSemiring α] [IsDomain α] (b₁ : α) (b₂ : α) (h₁ : b₁ ≠ 0) (h₂ : ¬IsUnit b₂) : Ideal.span {b₁ * b₂} < Ideal.span {b₁}

theorem Ideal.mul_mem_right {α : Type u} {a : α} (b : α) [CommSemiring α] (I : Ideal α) (h : a ∈ I) : a * b ∈ I

theorem Ideal.pow_mem_of_mem {α : Type u} {a : α} [CommSemiring α] (I : Ideal α) (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I

theorem Ideal.IsPrime.mul_mem_iff_mem_or_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {x : α} {y : α} : x * y ∈ I ↔ x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.pow_mem_iff_mem {α : Type u} [CommSemiring α] {I : Ideal α} (hI : Ideal.IsPrime I) {r : α} (n : ℕ) (hn : 0 < n) : r ^ n ∈ I ↔ r ∈ I

theorem Ideal.pow_multiset_sum_mem_span_pow {α : Type u} [CommSemiring α] [DecidableEq α] (s : Multiset α) (n : ℕ) : Multiset.sum s ^ (Multiset.card s * n + 1) ∈ Ideal.span ↑(Multiset.toFinset (Multiset.map (fun (x : α) => x ^ (n + 1)) s))

theorem Ideal.sum_pow_mem_span_pow {α : Type u} [CommSemiring α] {ι : Type u_1} (s : Finset ι) (f : ι → α) (n : ℕ) : (Finset.sum s fun (i : ι) => f i) ^ (s.card * n + 1) ∈ Ideal.span ((fun (i : ι) => f i ^ (n + 1)) '' ↑s)

theorem Ideal.span_pow_eq_top {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (n : ℕ) : Ideal.span ((fun (x : α) => x ^ n) '' s) = ⊤

theorem Ideal.isPrime_of_maximally_disjoint {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S) : Ideal.IsPrime I

theorem Ideal.neg_mem_iff {α : Type u} [Ring α] (I : Ideal α) {a : α} : -a ∈ I ↔ a ∈ I

theorem Ideal.add_mem_iff_left {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : b ∈ I → (a + b ∈ I ↔ a ∈ I)

theorem Ideal.add_mem_iff_right {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → (a + b ∈ I ↔ b ∈ I)

theorem Ideal.sub_mem {α : Type u} [Ring α] (I : Ideal α) {a : α} {b : α} : a ∈ I → b ∈ I → a - b ∈ I

theorem Ideal.mem_span_insert' {α : Type u} [Ring α] {s : Set α} {x : α} {y : α} : x ∈ Ideal.span (insert y s) ↔ ∃ (a : α), x + a * y ∈ Ideal.span s

@[simp]

theorem Ideal.span_singleton_neg {α : Type u} [Ring α] (x : α) : Ideal.span {-x} = Ideal.span {x}

theorem Ideal.eq_bot_or_top {K : Type u} [DivisionSemiring K] (I : Ideal K) : I = ⊥ ∨ I = ⊤

All ideals in a division (semi)ring are trivial.

def Ideal.equivFinTwo (K : Type u) [DivisionSemiring K] [DecidableEq (Ideal K)] : Ideal K ≃ Fin 2

A bijection between between (left) ideals of a division ring and {0, 1}, sending ⊥ to 0 and ⊤ to 1.

Equations

• One or more equations did not get rendered due to their size.

instance Ideal.instFiniteIdealToSemiring {K : Type u} [DivisionSemiring K] : Finite (Ideal K)

Equations

• (_ : Finite (Ideal K)) = (_ : Finite (Ideal K))

instance Ideal.isSimpleOrder {K : Type u} [DivisionSemiring K] : IsSimpleOrder (Ideal K)

Ideals of a DivisionSemiring are a simple order. Thanks to the way abbreviations work, this automatically gives an IsSimpleModule K instance.

Equations

• (_ : IsSimpleOrder (Ideal K)) = (_ : IsSimpleOrder (Ideal K))

theorem Ideal.eq_bot_of_prime {K : Type u} [DivisionSemiring K] (I : Ideal K) [h : Ideal.IsPrime I] : I = ⊥

theorem Ideal.bot_isMaximal {K : Type u} [DivisionSemiring K] : Ideal.IsMaximal ⊥

theorem Ideal.mul_sub_mul_mem {R : Type u_1} [CommRing R] (I : Ideal R) {a : R} {b : R} {c : R} {d : R} (h1 : a - b ∈ I) (h2 : c - d ∈ I) : a * c - b * d ∈ I

theorem Ring.exists_not_isUnit_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] (hf : ¬IsField R) : ∃ (x : R) (_ : x ≠ 0), ¬IsUnit x

theorem Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top {R : Type u_1} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤

theorem Ring.not_isField_iff_exists_prime {R : Type u_1} [CommSemiring R] [Nontrivial R] : ¬IsField R ↔ ∃ (p : Ideal R), p ≠ ⊥ ∧ Ideal.IsPrime p

theorem Ring.isField_iff_isSimpleOrder_ideal {R : Type u_1} [CommSemiring R] : IsField R ↔ IsSimpleOrder (Ideal R)

Also see Ideal.isSimpleOrder for the forward direction as an instance when R is a division (semi)ring.

This result actually holds for all division semirings, but we lack the predicate to state it.

theorem Ring.ne_bot_of_isMaximal_of_not_isField {R : Type u_1} [CommSemiring R] [Nontrivial R] {M : Ideal R} (max : Ideal.IsMaximal M) (not_field : ¬IsField R) : M ≠ ⊥

When a ring is not a field, the maximal ideals are nontrivial.

theorem Ideal.bot_lt_of_maximal {R : Type u} [CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : Ideal.IsMaximal M] (non_field : ¬IsField R) : ⊥ < M

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

The set of non-invertible elements of a monoid.

Equations

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

@[simp]

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

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

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

theorem zero_mem_nonunits {α : Type u} [Semiring α] : 0 ∈ nonunits α ↔ 0 ≠ 1

@[simp]

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

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

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