The lattice of ideals in a ring

Some basic results on lattice operations on ideals: ⊥, ⊤, ⊔, ⊓.

TODO

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

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

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

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.