instance Ideal.instIsTwoSidedMax_ado {R : Type u_1} [Semiring R] (I J : Ideal R) [I.IsTwoSided] [J.IsTwoSided] : (I ⊔ J).IsTwoSided

theorem Ideal.mul_eq_span_mul {R : Type u_1} [Semiring R] (I J : Ideal R) : I * J = span (↑I * ↑J)

theorem Ideal.pow_eq_span_pow_set {R : Type u_1} [Semiring R] (I : Ideal R) (n : ℕ) : I ^ n = span (↑I ^ n)

theorem Ideal.span_pow {R : Type u_1} [Semiring R] (S : Set R) (n : ℕ) [(span S).IsTwoSided] : span S ^ n = span (S ^ n)

theorem Ideal.mul_subset_mul {R : Type u_1} [Semiring R] (I J : Ideal R) : ↑I * ↑J ⊆ ↑(I * J)

theorem Ideal.pow_subset_pow {R : Type u_1} [Semiring R] (I : Ideal R) (n : ℕ) : ↑I ^ n ⊆ ↑(I ^ n)

theorem Ideal.sup_eq_span {R : Type u_1} [Semiring R] (I J : Ideal R) : I ⊔ J = span (↑I ∪ ↑J)

theorem Ideal.span_induction {R : Type u_1} [Semiring R] {s : Set R} {p : (x : R) → x ∈ span s → Prop} (mem : ∀ (x : R) (h : x ∈ s), p x ⋯) (zero : p 0 ⋯) (add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯) {x : R} (hx : x ∈ span s) : p x hx

@[simp]

theorem TwoSidedIdeal.fromIdeal_span {R : Type u_2} [Ring R] (S : Set R) : fromIdeal (Ideal.span S) = span S

theorem Ideal.le_toTwoSidedIdeal {R : Type u_2} [Ring R] {I : TwoSidedIdeal R} {J : Ideal R} [J.IsTwoSided] : I ≤ J.toTwoSided ↔ TwoSidedIdeal.asIdeal I ≤ J

theorem Ideal.toTwoSidedIdeal_le {R : Type u_2} [Ring R] {I : Ideal R} [I.IsTwoSided] {J : TwoSidedIdeal R} : I.toTwoSided ≤ J ↔ I ≤ TwoSidedIdeal.asIdeal J