LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Lattice

Imported Lean Pool material for LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Lattice.

@[simp]

theorem TwoSidedIdeal.ringCon_inj {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} : I.ringCon = J.ringCon ↔ I = J

@[simp]

theorem TwoSidedIdeal.ringCon_eq_top {R : Type u_1} [NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} : I.ringCon = ⊤ ↔ I = ⊤