HepLean Documentation

Mathlib.RingTheory.Ideal.Lattice

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 1I
theorem Ideal.mem_sup_left {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} :
x Sx S T
theorem Ideal.mem_sup_right {R : Type u} [Semiring R] {S : Ideal R} {T : Ideal R} {x : R} :
x Tx S T
theorem Ideal.mem_iSup_of_mem {R : Type u} [Semiring R] {ι : Sort u_1} {S : ιIdeal R} (i : ι) {x : R} :
x S ix 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 sx sSup S
theorem Ideal.mem_sInf {R : Type u} [Semiring R] {s : Set (Ideal R)} {x : R} :
x sInf s ∀ ⦃I : Ideal R⦄, I sx 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.