def Ideals.IsIdeal (R : Type u_1) [Ring R] (I : Set R) : Prop

def Ideals.principalIdeal (R : Type u_1) [CommRing R] (a : R) : Ideal R

@[implicit_reducible]

instance Ideals.instCommRingQuotient (R : Type u_1) [CommRing R] (I : Ideal R) : CommRing (R ⧸ I)

theorem Ideals.isMaximal_iff (R : Type u_1) [CommRing R] (I : Ideal R) : I.IsMaximal ↔ I ≠ ⊤ ∧ ∀ (J : Ideal R), I ≤ J → J = I ∨ J = ⊤