Documentation

Mathlib.RingTheory.TwoSidedIdeal.Lattice

The complete lattice structure on two-sided ideals #

Equations
theorem TwoSidedIdeal.sup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (J : TwoSidedIdeal R) :
(I J).ringCon = I.ringCon J.ringCon
theorem TwoSidedIdeal.mem_sup_left {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} {x : R} (h : x I) :
x I J
theorem TwoSidedIdeal.mem_sup_right {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} {x : R} (h : x J) :
x I J
theorem TwoSidedIdeal.mem_sup {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} {x : R} :
x I J yI, zJ, y + z = x
Equations
theorem TwoSidedIdeal.inf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) (J : TwoSidedIdeal R) :
(I J).ringCon = I.ringCon J.ringCon
theorem TwoSidedIdeal.mem_inf (R : Type u_1) [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {J : TwoSidedIdeal R} {x : R} :
x I J x I x J
Equations
theorem TwoSidedIdeal.sSup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)) :
(sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S)
theorem TwoSidedIdeal.iSup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} (I : ιTwoSidedIdeal R) :
(⨆ (i : ι), I i).ringCon = ⨆ (i : ι), (I i).ringCon
Equations
theorem TwoSidedIdeal.sInf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)) :
(sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S)
theorem TwoSidedIdeal.iInf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} (I : ιTwoSidedIdeal R) :
(⨅ (i : ι), I i).ringCon = ⨅ (i : ι), (I i).ringCon
theorem TwoSidedIdeal.mem_iInf (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} {I : ιTwoSidedIdeal R} {x : R} :
x iInf I ∀ (i : ι), x I i
theorem TwoSidedIdeal.mem_sInf (R : Type u_1) [NonUnitalNonAssocRing R] {S : Set (TwoSidedIdeal R)} {x : R} :
x sInf S IS, x I
Equations
@[simp]
theorem TwoSidedIdeal.mem_top (R : Type u_1) [NonUnitalNonAssocRing R] {x : R} :
Equations
theorem TwoSidedIdeal.mem_bot (R : Type u_1) [NonUnitalNonAssocRing R] {x : R} :
x x = 0
theorem TwoSidedIdeal.eq_top {R : Type u_2} [NonAssocRing R] (I : TwoSidedIdeal R) :
1 II =

Alias of the forward direction of TwoSidedIdeal.one_mem_iff.

theorem TwoSidedIdeal.one_mem {R : Type u_2} [NonAssocRing R] (I : TwoSidedIdeal R) :
I = 1 I

Alias of the reverse direction of TwoSidedIdeal.one_mem_iff.